Generation and truth values in a topos — Lean formalisation

This repository accompanies the note Generation and truth values in a topos by Sam van Gool (note/vangool_generation_topos_2026.tex). It contains a formalisation in Lean 4 and Mathlib of the results of the note. The main theorem, PittsNegative.pitts_negative, corresponding to Corollary 5 in the note, states that the free Heyting algebra on two generators is not the algebra of subterminals of any elementary topos, which is the main result of Xu and Ye [XY], although our proof here resembles more the proof of Kocsis [K], and our own reworking.

The artefact is archived at https://doi.org/10.5281/zenodo.23185917 and available at https://github.com/samvang/generation_topos (tag v1).

note/vangool_generation_topos_2026-lean.tex is the same note in which phrases link to the corresponding Lean declarations (see The annotated note).

Provenance

The Lean code was first developed by I. Shillito with a grant of access to OpenAI models through the ChatGPT for Academic Researchers program. Further AI assistance was used for developing this code and accompanying documentation, while the TeX is exclusively human-written.

The construction of finite colimits in challenge/ToposFiniteColimits.lean follows Paré's proof as presented in [BW, §5.1], and Bhavik Mehta's Lean 3 development of power objects (https://github.com/b-mehta/topos). Images in challenge/ToposImages.lean are constructed as in [F, §2.1].

Contents

• challenge/: the statement of pitts_negative (Challenge.lean, where it is admitted with sorry) and the definitions needed to state it: elementary toposes, the Heyting algebra of subterminals, and freeness on two generators.
• solution/: the proofs; Solution.lean proves pitts_negative.
• note/: the note, the annotated note, and the scripts that generate the annotated note and its links.
• config.json: configuration for checking the solution against the challenge with Comparator.
• docbuild/: generation of HTML documentation with doc-gen4.

Correspondence between TeX and Lean

Note	Lean declaration	File
finite element, separating set	Quasi.IsFiniteElt, Quasi.FinSeparating	solution/QuasiBounds.lean
Definition: quasi-supremum, quasi-infimum	Quasi.IsQuasiSup, Quasi.IsQuasiInf	solution/QuasiBounds.lean
finitary object; Ω is finitary	Topos.Finitary, Topos.finitary_Ω	solution/QuasiTopos.lean, solution/QuasiOmega.lean
Cl_𝓕; γ; ∀x, γ(x) → P(x); ∃x, γ(x) ∧ P(x)	Topos.ExtClosure, Topos.internalClosure, Topos.forallObs, Topos.existsObs	solution/ToposClosure.lean
Theorem thm:quasi	Topos.isQuasiInf_forallObs, Topos.isQuasiSup_existsObs	solution/QuasiTopos.lean
Corollary cor:kocsis	Topos.exists_isQuasiInf_himp	solution/QuasiOmega.lean
characteristic formulas	IsF₂On.exists_deJongh	solution/DeJonghFinite.lean
Lemma lem:no-inf	IsF₂On.not_isQuasiInf	solution/NoQuasiInf.lean
Corollary cor:yexu	pitts_negative	solution/Solution.lean
concluding remarks	IsF₂On.finSeparating, IsF₂On.not_isGLB	solution/DeJonghFinite.lean, solution/NoQuasiInf.lean

The formalisation differs from the note in a few presentational respects:

• Quasi-bounds are defined by quantifying over the lower (upper) bounds of {u ⊓ s | s ∈ S} instead of using its finite meet (join); the two are equivalent.
• Predicates are subobjects P of X rather than morphisms X ⟶ Ω, so the set S lives in Sub(1) rather than E(1, Ω).
• In the proof of Theorem thm:quasi, a finite union of the classes {x | u → x = tᵢ} plays the role of the internal term I.

Building

Install elan; it installs the Lean version in lean-toolchain (v4.35.0-rc3). Mathlib is pinned in lake-manifest.json. Then, in this directory:

lake exe cache get      # download compiled Mathlib (needs network access)
lake build              # check the challenge and the solution
lake env lean solution/ProofAudit.lean   # print the axioms used

All results depend only on the axioms propext, Classical.choice and Quot.sound, and solution/ contains no sorry.

Comparator (optional) checks that Solution proves exactly the statement in challenge/Challenge.lean using only the axioms in config.json; see its README for building comparator, lean4export and landrun, then run lake env <path>/comparator config.json.

HTML documentation (optional): cd docbuild && lake build Solution:docs, then open docbuild/.lake/build/doc/index.html.

The annotated note

note/vangool_generation_topos_2026-lean.tex is generated from the note by note/make_lean_tex.py. It differs from the note only by one block of macro definitions, the text of the footnote about Lean, and \lnk{Decl}{…} links around existing text.

References

• [vG] S. van Gool, Generation and truth values in a topos, 2026 (this note).
• [XY] Y. Xu, L. Ye, Failure of higher-order truth within intuitionistic propositional logic, arXiv:2608.26874v2, 2026.
• [K] Z. A. Kocsis, Two applications of the point-free coderivative, arXiv:2609.29436v1, 2026.
• [P] A. M. Pitts, On an interpretation of second-order quantification in first-order intuitionistic propositional logic, J. Symbolic Logic 57(1), 33–52, 1992.
• [B] N. Bezhanishvili, Lattices of intermediate and cylindric modal logics, PhD thesis, University of Amsterdam, 2006.
• [BW] M. Barr, C. Wells, Toposes, Triples and Theories, §5.1.
• [F] P. Freyd, Aspects of topoi, Bull. Austral. Math. Soc. 7, 1972, §2.1.
• [Mathlib] The Mathlib Community, The Lean mathematical library, CPP 2020.

Licence

The Lean code and scripts are distributed under the Apache License 2.0 (see LICENSE).