Jump to content

Lean theorem prover/Bibliography: Difference between revisions

From The Invariance Itself

PMA Publisher (talk | contribs)

1 user group
288 edits
PMA Publisher (talk | contribs)
approved
288 edits
Published from the Principia Machina source
 
PMA Publisher (talk | contribs)
approved
288 edits
Published from the Principia Machina source
 
Line 1: Line 1:
{{DISPLAYTITLE:Bibliography}}
{{DISPLAYTITLE:Bibliography}}
{{Lean theorem prover map}}


Every work cited on the pages of this edition, listed once, with the pages that cite it in reading order. There are 277: 86 papers and books; 114 items of Lean documentation and source, 52 of them parts of the reference manual; 64 project pages and announcements; and 13 press articles and encyclopedia entries.
Every work cited on the pages of this edition, listed once, with the pages that cite it in reading order. There are 277: 86 papers and books; 114 items of Lean documentation and source, 52 of them parts of the reference manual; 64 project pages and announcements; and 13 press articles and encyclopedia entries.

Latest revision as of 19:35, 15 October 2026

Lean theorem prover: map
Reading the edition
Three levels of reading
Glossary
Notation
Chronology
Reading by level
Start here: What a proof assistant does
The type theory: Terms, types and judgments
How Lean works: Elaboration
The history: Automath
The applications: Research mathematics
Sources
Sources
Bibliography
Further reading
Related
The move to Lean

Every work cited on the pages of this edition, listed once, with the pages that cite it in reading order. There are 277: 86 papers and books; 114 items of Lean documentation and source, 52 of them parts of the reference manual; 64 project pages and announcements; and 13 press articles and encyclopedia entries.

Two citations are taken to be one work when they share a DOI, an arXiv number or a web address. A preprint and its published version are listed apart when the pages cite them apart, and so is each version of a document that changes with Lean: a chapter of the reference manual cited in its edition for Lean 4.34.0 on some pages and for Lean 4.35.0 on others appears twice, once under each address.

Where pages cite one work in different forms, the form given here is the fullest, and a note says what differs when it is more than punctuation, capitals or the sections a page names. The 19 works that were not read, or were read only in part, are marked; the sources page says what each one carries and what carries it instead.

Papers and books

Lean documentation and source

The Lean Language Reference

Other documentation and textbooks

Source code

Projects and announcements

Press and encyclopedias

Next

References

  1. ↑ Terms, types and judgments gives the journal as Indagationes Mathematicae (Proceedings) 75 (5); Automath gives both numberings, as above.
  2. ↑ The Calculus of Constructions cites the PDF attached to the release, as a thesis of April 2019; the other pages cite the release page.
  3. ↑ Checking a proof again later, What has to be trusted and Consistency and the metatheory cite version 3 of the arXiv text, of 14 September 2025. The paper's TYPES 2025 version is listed separately; Definitional equality, Inductive types and recursors and Terms, types and judgments cite that version and say they read version 2 of the arXiv text.
  4. ↑ Definitional equality, Inductive types and recursors and Terms, types and judgments say they read the text in arXiv version 2; Two kinds of equality calls the arXiv text a preprint, Proof export and independent checkers its full version. Version 3 of the arXiv text is listed separately.
  5. ↑ Read for Universes and Prop; The Calculus of Constructions cites it from its bibliographic record.
  6. ↑ LCF and the tactic idea and Martin-Löf type theory cite the author's PDF copy, www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf, under the name Mike Gordon; Automation and its limits and Tactics cite the HTML copy given here.
  7. ↑ Read for Universes and Prop; Martin-Löf type theory cites it from its bibliographic record.
  8. ↑ Principia Machina, Tactics, What a proof assistant does and Why there is no type of all types give the title without "(System Description)"; Inductive types and recursors, Programs and proofs in one language and The small trusted core omit the volume number 12699.
  9. ↑ The same notes, in the edition of the manual for Lean 4.34.0, are listed above, cited on The compiler and runtime. This citation uses the address under "latest", which follows the newest version.
  10. ↑ LCF and the tactic idea cites the chapter at its earlier address, lean-lang.org/theorem_proving_in_lean4/tactics.html, which now forwards here.
Retrieved from "https://invarians.org/index.php?title=Lean_theorem_prover/Bibliography&oldid=6820"