Medvedev's logic of finite problems (1962) shown undecidable; key idea from ChatGPT Sol 5.6, central argument checked in Lean by Claude Opus 5
Rodrigo Nicolau Almeida and Søren Brinck Knudstorp proved that Medvedev's logic of finite problems, a well-known superintuitionistic logic, is undecidable, which settles what they call a longstanding open problem (arXiv 2609.13359, 11 Sep 2026). They reduce the periodic tiling problem to it. The authors 'do not take any credit' for the key ideas: ChatGPT Sol 5.6 obtained them on 4 Sep 2026, and Claude Opus 5 produced a Lean verification of the central argument. All prompts and model outputs are published.
Key facts
- Medvedev introduced the logic of finite problems in 1962 (Dokl. Akad. Nauk 142); whether it is decidable was a longstanding open question
- Main theorem: Medvedev's logic ML is undecidable, via a reduction from periodic tiling to non-theoremhood; similarly Skvortsov's logic of infinite problems is undecidable, and the two logics are separated by any aperiodic tiling of the plane
- Methodology §7: 'the key idea for the undecidability of ML – namely the construction of the tiling posets P_W, and the encoding of the reduction – was obtained by prompting ChatGPT Sol 5.6 … whilst the authors assume responsibility for the correctness of the results, they do not take any credit in such ideas'
- The authors rewrote the text themselves and invoke the Leiden Declaration; Claude Opus 5 was used for proofreading and for a Lean verification of the main central argument; prompts, preliminary documents and verification ledgers are public on the first author's website
- Status: preprint (32 pages)
Science result
- Field
- mathematics / mathematical logic / superintuitionistic logics
- Problem
- Decidability of Medvedev's logic of finite problems (open since 1962)
- Result
- Medvedev's logic (and Skvortsov's logic) is undecidable.
- AI system
- GPT-5.6 Sol (ChatGPT), Claude Opus 5
- Human role
- Humans chose the problem and wrote structured prompts; ChatGPT found the core construction; the humans checked and rewrote it
- Verification
- Lean verification of the central argument (by Claude Opus 5) plus author checking; preprint
- Status
- confirmed
What happened
Two logicians, one of whom wrote his PhD on undecidability, suspected a targeted search could settle Medvedev's logic. They prompted ChatGPT Sol 5.6, which returned a tiling-based reduction on 4 September. Claude Opus 5 formalised the central argument in Lean, and the authors wrote the paper and published the whole prompt trail.
Why it matters
It answers a well-known question in non-classical logic, and it is a model of transparent disclosure: full prompt and output archives are published alongside the paper and treated like a dataset.
Changelog
- 2026-09-30: created
Related events
- OpenAI broadly releases GPT-5.6 (Sol, Terra, Luna) after government-gated preview ★★★★
- Anthropic releases Claude Opus 5 — near-Fable-5 intelligence at half the price ★★★★
- Leiden Declaration on Artificial Intelligence and Mathematics sets community norms for AI in maths (4,000+ signatories) ★★★
- Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help (July–September catalogue) ★★★★
Sources (1)
id: 2026-09-11-medvedev-logic-undecidable · updated 2026-09-30 · open in the interactive timeline