Medvedev logic is undecidable
Is Medvedev logic —the intuitionistic logic of finite problems—decidable, and can it be recursively axiomatized?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Intuitionistic logic; computability theory; tiling problems
- Posed by
- Implicit by Yuri Medvedev (1962), explicitly by Maksimova et al 1979
- Year posed
- 1979
- Years open
- 47y
- Solved
- 2026-09-11
- Model
- ChatGPT Sol 5.6; Claude Opus 5
- Vendor
- OpenAI; Anthropic
- Collaborators
- Rodrigo Nicolau Almeida, Søren Brinck Knudstorp; Pawel Pawlowski
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- —
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The paper reduces periodic plane tiling to non-theoremhood in Medvedev logic and proves is undecidable and not recursively axiomatizable. A modification also proves undecidability of Skvortsov logic for infinite problems, and shows the two logics can be separated using any aperiodic plane tiling. Both papers are preprints, so the result should remain a review-pending candidate.
What the AI did
ChatGPT Sol 5.6 generated the central idea and technical development, including the tiling poset and reduction from periodic plane tiling. Claude Opus 5 produced the Lean formalization. The authors report obtaining the first result on 4 September, then checking the literature and consequences, organizing the argument, and writing the paper; prompts and development records are public.
Verification
The authors report the main reduction argument was checked in Lean. The preprint has not been peer reviewed, and this submission does not independently audit that the formal statement exactly matches every informal claim. Paweł Pawłowski independently announced essentially the same undecidability conclusion almost simultaneously, but that does not amount to cross-verification of all details of either proof.
Sources
- PaperarXiv preprint
- Lean proofPawlowski's Lean formalization of the proof
- Independent workIndependent near-simultaneous result
- Problem recordMaksimova et al 1979 (in Russian) - Problem statement
Submitted by BoldPanther302 on