Revision #1267 → #2407 · back to history
addedChurch's theorem (Entscheidungsproblem unsolvable)d1894c5fa6e7
addedInaccessible cardinal yields a model of ZFC83162240aaa0
addedWellfoundedness of ε₀788b578a3ae4
addedGraph minor theorem (Robertson–Seymour)bec6a0784b08
modifiedHalting problem undecidable242c13dd506d
| Field | From #1267 | To #2407 |
|---|
| mathlib.decl | Nat.Partrec.Code.halting_problem | ComputablePred.halting_problem |
| note | `halting_problem` proves the predicate deciding whether a code halts on input n is not computable. | `ComputablePred.halting_problem` proves that deciding whether a code halts on input n is not computable. |
modifiedMatiyasevich's theorem81d6ddc1c8b4
| Field | From #1267 | To #2407 |
|---|
| mathlib.decl | pow_dioph | Dioph.pow_dioph |
| note | Mathlib formalizes a key MRDP step (`pow_dioph`, the power function is Diophantine) but not the full theorem or the undecidability of Hilbert's tenth problem. | Mathlib formalizes a key MRDP step (`Dioph.pow_dioph`, the power function is Diophantine) but not the full theorem or the undecidability of Hilbert's tenth problem. |
addedCantor's diagonal argument32c9824ad872