कक्षा 9–12Computationपाठ उपलब्ध
First steps in Lean
Stating and proving simple results in the Lean 4 proof assistant: propositions and proofs, rewriting, induction on natural numbers and reading Mathlib statements, with attention to what a machine check does and does not guarantee.
math.comp.intro-lean
इस पर आधारित
Propositional logic and truth tablesProof: direct, contrapositive, contradiction and inductionProgramming for mathematics
15 अनिवार्य पूर्वापेक्षाएँ (बिल्कुल नीचे तक)
आप सीखेंगे
- Write and check short Lean proofs of propositional tautologies and simple equalities using rfl, rw and simp.
- Prove a statement about natural numbers by induction in Lean, such as 0 + n = n.
- Read a Mathlib theorem statement, and distinguish applying a library theorem from proving a result independently.
परिभाषा
- A proof assistant is a program that checks proofs written in a formal language.
- In Lean, a proposition is a type and a proof of it is a term of that type.
- A tactic is a command that builds part of a proof, such as rw (rewrite) or induction.
प्रमेय
- A Lean proof that compiles without sorry and without added axioms has been checked by Lean's kernel relative to Lean's logic.
- A formal proof is only as meaningful as its formal statement: a mis-stated theorem can be proved correctly.
- For Lean's natural numbers, n + 0 = n holds by definition (rfl), while 0 + n = n needs a proof by induction.
आम भ्रांतियाँ
- Believing a machine-checked proof guarantees that the statement says what was intended.
- Thinking a proof containing sorry is finished.
- Confusing the use of a Mathlib lemma with proving the result from more basic facts.
आगे ले जाता है
वैकल्पिक खोजें
- Type theory and propositions as types Lean's logic is a dependent type theory in which propositions are types and proofs are terms.
अधिगम पथ
आगे पढ़ने के लिए
- Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, Theorem Proving in Lean 4
- Jeremy Avigad and Patrick Massot, Mathematics in Lean