A 21-state Turing machine for… to Strengthened V0 Bounded…

TheoremA 21-state Turing machine for Goldbach's conjecture#

A concrete 21-state binary Turing machine halts on the blank tape exactly when Goldbach's conjecture is false. The proof connects it to the earlier 25-state machine, verifies both machines' prime-search semantics, and preserves finite-machine execution, tape-scanning and reachability infrastructure. This imports only the Goldbach dependency closure of Cryptids, excluding its Riemann, ZF and Busy Beaver developments.

Quoted from the card LeanPool/projects/cryptids-goldbach.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanConjectureMachines.Goldbach21.Semantics.halts_candidate_iff_not_goldbach

TheoremA formalization of Borel determinacy in Lean#

Formalizes Martin's theorem that every Borel Gale-Stewart game is determined.

Quoted from the card LeanPool/projects/a-formalization-of-borel-determinacy-in-lean.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanGaleStewartGame.borel_determinacy · GaleStewartGame.Games.borel_determinacy

TheoremCraig interpolation and Beth definability for propositional dynamic logic#

Proves Craig interpolation for full propositional dynamic logic, including tests and Kleene star, by constructing interpolants from uniform cyclic tableaux. Interpolants use only atomic propositions and atomic programs common to the two formulas. The development also proves the local Beth definability property for a propositional letter, and supplies reusable syntax, Kripke semantics, Fischer-Ladner closure, tableau soundness and completeness, finite reachability and game-theoretic infrastructure. The results assert existence; no executable extraction algorithm or complexity bound is claimed. Human contributors and Aristotle jointly developed the formalization. The completeness modules reuse the finite game determinacy theorem already pooled in LeanPool.Lean4GlCoalgebras instead of duplicating it.

Quoted from the card LeanPool/projects/pdl-craig-interpolation.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • PDL.interpolation (theorem; a main declaration), declared in LeanPool/PDL/Interpolation/Theorem.lean, line 27: “If the implication from PDL formula phi to psi is valid in every Kripke model, there exists a PDL formula theta whose atomic proposition and program vocabulary is contained in the intersection of theirs, such that phi implies theta and theta implies psi in every model.”
  • PDL.beth (theorem; a main declaration), declared in LeanPool/PDL/Beth.lean, line 29: “If a PDL formula phi implicitly determines a propositional letter p (all two-letter substitutions agree wherever both substituted formulas hold), there is a formula psi using only phi's vocabulary other than p such that phi entails that p is equivalent to psi.”
  • PDL.consIffSat (theorem), declared in LeanPool/PDL/Completeness/Theorem.lean, line 152: “A free sequent is tableau-consistent if and only if it is satisfiable in a Kripke model.”
Project
  • Authors: PDL formalization contributors.
  • Contributors: Malvin Gattinger, Madeleine Gignoux, Noam Cohen, Haitian Wang, Wietse Bosman, Xiaoshuang Yang, Amos Nicodemus, Andrés Goens, DdosSantosGomes, Eshel Yaron, Dionysis Yusofy.
  • Source: Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof by Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema, arXiv:2503.13276.
  • Project repository: m4lvin/lean4-pdl, at commit ec3b050e.
  • Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
  • License: Apache-2.0.
  • MSC2020: 03B45, 03B70, 03F03.
  • In Lean Pool: LeanPool/PDL, from the card LeanPool/projects/pdl-craig-interpolation.yaml.
Sources
LeanPDL.interpolation · PDL.beth

TheoremCraig Interpolation for Gödel-Löb logic via coalgebraic proofs#

Formalizes a proof-theoretic Craig interpolation theorem for Gödel-Löb provability logic, built on a coalgebraic notion of circular proof.

Quoted from the card LeanPool/projects/lean4-gl-coalgebras.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLean4GlCoalgebras.interpolation

StructureDomainTheory#

Formalizes Dana Scott's domain theory through Scott information systems and PRG-19 neighbourhood systems, including approximable maps, products, function spaces, fixed points, recursive presentations, and initial-algebra constructions for denotational semantics.

Quoted from the card LeanPool/projects/domain-theory.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanInfoSys · Domain.Neighborhood.NeighborhoodSystem

ClassFirst Order Language of ZF Set Theory#

Formalizes ZF set theory inside Lean's FirstOrder.Language framework, enabling meta-mathematical arguments such as elementary submodels.

Quoted from the card LeanPool/projects/fo-zfc.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanFirstOrder.ZFC.ModelZF · FirstOrder.ZFC.ext_induction

TheoremGlobal completeness of one-sorted definedness-free matching logic#

Formalizes the one-sorted case of Chen and Roșu's global-completeness argument and independently discharges its local-completeness oracle by mechanizing the canonical-model construction from their 2019 Matching μ-Logic technical report (Theorem 73, Lemmas 80–81, and strong local completeness Theorem 83). The resulting theorem supplies both local completeness and soundness for countably infinite variable types.

Quoted from the card LeanPool/projects/matching-logic-completeness.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanMatchingLogic.global_completeness_entryIII

TheoremGödel's First and Second Incompleteness Theorems#

Formalizes Gödel's first and second incompleteness theorems for first-order arithmetic, building on formalized arithmetization and provability-logic infrastructure.

Quoted from the card LeanPool/projects/incompleteness.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.Incompleteness.goedelFirst · LeanPool.Incompleteness.goedelSecond

TheoremInfinitary logic and countable model theory#

Formalizes the syntax and semantics of infinitary logic and a broad collection of its classical theorems: Scott sentences and ranks, Karp's theorem, model existence, the sharp Morley--Hanf bound, Craig, Lyndon, and Malitz interpolation, López--Escobar definability, undefinability of well-ordering, the Silver--Burgess and Morley counting dichotomies, and an honest coded-fragment interface whose HF compactness theorem is derived from first-order compactness.

Quoted from the card LeanPool/projects/infinitary-logic.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 31 main results, each with its informal statement quoted from the card. The scan finds 31 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanFirstOrder.Language.scottSentence_characterizes

TheoremThe Kunen inconsistency theorem#

Formalizes elementary embeddings of models of ZF set theory and proves the Kunen inconsistency theorem, that there is no nontrivial elementary embedding of the set-theoretic universe into itself.

Quoted from the card LeanPool/projects/settheory.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanSetTheory.kunen_inconsistency_V · NontrivialElementaryEmbedding

DefinitionLentil: Temporal Logic of Actions in Lean 4#

A shallow embedding of Leslie Lamport's Temporal Logic of Actions (TLA) in Lean 4, with the temporal modalities, standard propositional and temporal proof rules, weak-fairness and leads-to reasoning, and an interactive proof mode for TLA judgments.

Quoted from the card LeanPool/projects/lentil.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanTLA.always · TLA.eventually · TLA.always_induction · TLA.wf1

TheoremNash-Williams fronts and 2-better-quasi-orders#

Formalizes Nash-Williams fronts through their well-founded prefix trees and ordinal ranks, proves the finite-color Nash-Williams theorem, and derives the infinite Ramsey theorem for arbitrary finite arity. The order-theoretic development proves that 2-better-quasi-orders are well-quasi-orders and establishes closure under finite products, lexicographic sums, domination of subsets, and pointwise embedding of sequences. Throughout, TwoBQO r is the good-triple property of an arbitrary binary relation r (every pair-sequence has m < n < l with f(m,n) related to f(n,l)); it assumes no reflexivity or transitivity of r.

Quoted from the card LeanPool/projects/nash-williams.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanFront.IsFront.nash_williams · TwoBQO.wellQuasiOrdered

TheoremNew Foundations refutes the Weak Partition Principle#

Constructs a formal first-order derivation of the negation of the Weak Partition Principle from New Foundations, with extensionality and the full integer-stratified comprehension schema. Proves full deductive equivalence with Metamath's Hailperin-derived finite presentation, including its added singleton axiom. Replays the source proof through nominal syntax, explicit freshness certificates, and a de Bruijn calculus. Includes reusable first-order soundness and completeness, stratification, lowering, and proof-translation infrastructure. This is a derivability theorem; it does not assert the consistency of New Foundations.

Quoted from the card LeanPool/projects/nf-weak-partition.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • NFChoice.Foundation.NFStandard.NF_proves_not_WPP (theorem; a main declaration), declared in LeanPool/NFWeakPartition/NFStandard/NotWPP.lean, line 27: “Standard New Foundations formally derives the negation of WPP. WPP says that, for all sets x and y, if a function maps y onto x and an injective function maps y into x, then an injective function maps x into y.” Its source, as the card gives it: “Upstream Proof/NFStandard/NotWPP.lean and the exact source formulation documented in README.md at the pinned commit. Standard-NF completion: commit a9f9867ee379835f91a4f05f9c4a352d44ca1775, 2026-08-25 00:16:27 UTC. Palomar registration PALOMAR-2026-08-27-000005 is dated 2026-08-27, without a verified time of day. The responsible public maintainer is Elliot Glazer. Upstream Flypitch4 credits Ian Klatzco and Claude for its Lean 4 port; this import also includes AI-assisted porting and proof repairs, hence mixed provenance. The deterministic Metamath replay is not by itself evidence of AI mathematical authorship. Independent novelty is not claimed by this card.”
  • NFChoice.Foundation.NFStandard.nf_hailperin_deductivelyEquivalent (theorem), declared in LeanPool/NFWeakPartition/NFStandard/Equivalence.lean, line 68: “Extensionality together with every integer-stratified comprehension instance and Metamath's Hailperin-derived finite first-order presentation, including its added singleton axiom, derive exactly the same sentences.” Its source, as the card gives it: “Upstream Proof/NFStandard/Equivalence.lean at the pinned commit. Metamath's ax-sn entry credits the singleton addition to SF on 2015-01-12 and distinguishes it from Hailperin's original presentation: https://us.metamath.org/nfeuni/ax-sn.html.”
Project
  • Authors: Elliot Glazer, NFNotWPP contributors, Jesse Michael Han, Floris van Doorn, Ian Klatzco.
  • Source: NF proves not-WPP, source-complete Lean formalization.
  • Project repository: elliotglazer/nf-not-wpp, at commit fa58a7a8.
  • Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
  • License: Apache-2.0.
  • MSC2020: 03E70, 03B35.
  • In Lean Pool: LeanPool/NFWeakPartition, from the card LeanPool/projects/nf-weak-partition.yaml.
Sources
LeanNFChoice.Foundation.NFStandard.NF_proves_not_WPP

TheoremThe nonmeagre lower bound for the rearrangement number#

Formalizes the inequality non(M) ≤ rr in ZFC via relational systems, category and slalom bounds, finite-vector constructions, and rearrangements of conditionally convergent real series. The reverse inequality from the accompanying manuscript is outside the upstream Lean formalization.

Quoted from the card LeanPool/projects/rr-equals-nonmeager-paper.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanNonMRR.nonM_le_rr

InductiveOracle Computability and Turing Degrees#

Formalizes oracle-relative computability via partial recursive functions, Turing reducibility and the Turing degrees as an upper semilattice, a Gödel numbering with a universal oracle machine, the jump operator, and the arithmetical hierarchy.

Quoted from the card LeanPool/projects/computability.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanComputability.RecursiveIn · Computability.TuringDegree

TheoremOrdered resource algebras and the Iris recursive domain model#

Constructs the algebraic core of the Iris proposition model from complete step-indexed spaces, ordered resource algebras, finite-support ghost maps, and monotone predicates. Proves guarded fixed-point unfolding and uniqueness, solves contractive mixed-variance domain equations, and constructs mutually inverse folding and unfolding maps for the recursive proposition model. Includes the October 2026 ordered-resource generalization and reusable morphism, product, optional-resource, and frame-preserving update infrastructure. The import is the mathematical dependency closure of IProp; it does not include the proof mode, HeapLang, program logics, or claims about their soundness.

Quoted from the card LeanPool/projects/iris-algebra.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
  • Authors: The Iris-Lean Contributors.
  • Contributors: Mario Carneiro, Sebastian Graf, Sergei Stepanenko, Markus de Medeiros, Zongyuan Liu, Puming Liu, Janine Lohse, Сухарик (@suhr).
  • Source: Iris in Lean and the ordered resource algebra extension, arXiv:2609.24252.
  • Project repository: leanprover-community/iris-lean, at commit 81bc3508.
  • Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
  • License: Apache-2.0.
  • MSC2020: 03B70, 68Q55, 68N30.
  • In Lean Pool: LeanPool/IrisAlgebra, from the card LeanPool/projects/iris-algebra.yaml.
Sources
LeanIris.IProp.fold_unfold · Iris.IProp.unfold_fold

ClassPartial Combinatory Algebras#

Formalises partial combinatory algebras with the K/S combinators, programming combinators, the free combinatory algebra, and the graph model.

Quoted from the card LeanPool/projects/partial-combinatory-algebras.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.PartialCombinatoryAlgebras.PCA

TheoremPCF Theory#

Formalizes foundational results from Shelah's Possible Cofinality theory, including the existence of club-guessing sequences.

Quoted from the card LeanPool/projects/pcf-theory.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
  • Authors: YnirPaz.
  • Source: doi:10.1007/978-1-4020-5764-9_15.
  • Project repository: YnirPaz/PCF-Theory.
  • Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
  • License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0. Lean Pool's notice file notes: “The upstream MIT LICENSE file contains no copyright line; the repository owner of record is "YnirPaz".”
  • MSC2020: 03E04, 03E10, 03E55.
  • In Lean Pool: LeanPool/PCFTheory, from the card LeanPool/projects/pcf-theory.yaml.
Sources
LeanOrdinal.exists_isClubGuessing_of_cof_uncountable

AliasPointwise provable equality and the failure of composition#

For every consistent recursively enumerable extension of Peano arithmetic, pointwise provable equality of unary programs fails to respect composition. Separate productive-set and Goedel incompleteness proofs establish the obstruction. For consistent extensions, compatibility is equivalent to Pi-one completeness. For every extension, the generated composition congruence is extensional equality in the Sigma-one sound case and universal otherwise. The development also proves weak-totality and range obstructions and identifies the sound generated quotient with actual unary partial recursive functions. Its coherent dependency closure preserves the concrete evaluator, arithmetization, first-order syntax, semantics and provability infrastructure. Main-result proofs were produced by AI agents under Florian Lengyel's direction; the Foundation dependency includes substantial human formalization by the Formalized Formal Logic contributors.

Quoted from the card LeanPool/projects/pointwise-provable-composition.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanPointwiseComposition.no_quotient_of_enumerable_axioms

TheoremStrengthened V0 Bounded Arithmetic Interfaces#

Formalizes first-order and two-sorted bounded-arithmetic model infrastructure, including arithmetic model laws and string-addition laws for strengthened bundled V0-style interfaces with propositional induction, order, cancellation, decidability, and algebraic laws assumed as fields rather than derived from a separate raw V0 class.

Quoted from the card LeanPool/projects/formalization-of-bounded-arithmetic.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 9 main results, each with its informal statement quoted from the card. The scan finds 9 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanV0Model.ind_strengthened_v0 · str_add_assoc_strengthened_v0

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.