The Lean Theorem Prover (System Description)¶
de Moura, L., Kong, S., Avigad, J., van Doorn, F., & von Raumer, J. (2015). The Lean Theorem Prover (System Description). Automated Deduction – CADE-25.
Cited by¶
1 citation across 1 artifact.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Enthymeme
- A proof assistant like Coq or Lean is the limiting case where the assumption base is forced to zero: every premise must be stated, so the enthymeme is eliminated by construction.
This sourceDescribes an interactive proof assistant whose kernel checks every inference step against the axioms — supporting that proof assistants force every premise to be stated, eliminating the enthymeme by construction.
- A proof assistant like Coq or Lean is the limiting case where the assumption base is forced to zero: every premise must be stated, so the enthymeme is eliminated by construction.
Verification¶
This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.
Registry ID ref:4304400d9772 · see in the full table