AI-assisted undecidability of Medvedev logic
Almeida and Knudstorp report that Medvedev’s logic of finite problems is undecidable, by reducing periodic plane tiling to non-theoremhood.
Original report: 2026-09-11Mathematical logic and foundations
Logic studies formal languages, models, and computability.
Progress records 3
Understand the topics ↓3 records · Includes focused interests · How we rate progress
AI-assisted lower bound for resolution over parities
Braun reports more than exp(n/(32768ℓ²)) clauses for DAG-like Res(⊕) refutations of the bit pigeonhole principle, for n=2^ℓ and ℓ≥32, without depth or regularity restrictions.
Original report: 2026-09-19OpenAI reports: Shelah’s eventual categoricity conjecture
OpenAI claims that every infinite Löwenheim–Skolem bound admits a uniform threshold above which one categorical cardinal forces categoricity throughout the remaining tail, in ZFC.
Read original source Pinned primary manuscript · family 240github.com
Original report: 2026-10-06Understanding the topics
Read the background
Logic studies formal languages, models, and computability. A theorem in ZFC, a conditional result, and an independence claim have different meanings.
Specific problems in this topic
- Decidability of Medvedev logic
- Resolution-over-parities proof complexity
- Shelah’s eventual categoricity conjecture
Background review: 2026-10-11. Selected sources:
Website timeline
Publication dates and editorial changes.