Medvedev’s logic of finite problems (1962) shown undecidable

Your AI and this story

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)
• Follow-up: Han Xiao (arXiv 2609.39577, 30 Sep 2026) proves the logic Cheq is not finitely axiomatizable (a human result ‘established before the rise of AI’) and that Medvedev’s undecidability implies Cheq’s; the paper notes Theorem 6.2 ‘does use the AI-generated proof that Medvedev logic is undecidable’
• AI disclosure (abstract, arXiv 2609.13359): ‘The core idea and technical work of the undecidability proof were obtained using ChatGPT Sol 5.6, and formally verified in Lean by Claude Opus 5.’ arXiv comment: ‘main result obtained via LLM (see methodology section)’