ImperialCollegeLondon / M40001_leanLinks
Lean 3 material related to Imperial College's "Introduction to University Mathematics" course
β161Updated last year
Alternatives and similar repositories for M40001_lean
Users that are interested in M40001_lean are comparing it to the libraries listed below
Sorting:
- π§ Liquid Tensor Experimentβ199Updated last year
- Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTTβ128Updated last year
- This project converts structured Lean code into an interactive browser game.β77Updated last year
- Lean 3 material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics. Lean 4 version available here: https://github.com/Impβ¦β119Updated last year
- β164Updated 5 years ago
- Lean for the Curious Mathematician 2020β67Updated last year
- A gamification of the theorems in MATH40002 Analysis 1β82Updated 2 years ago
- Lean Library currently studying for a degree at Imperial Collegeβ226Updated 4 months ago
- Lecture notes for a course on writing proofs, on paper and in the Lean proof assistantβ262Updated 6 months ago
- β251Updated 3 months ago
- Source code for the Mathematics in Lean tutorial.β153Updated last week
- A simple raytracer written in Lean 4β138Updated last year
- The agda-unimath libraryβ257Updated this week
- Perfectoid spaces in the Lean formal theorem prover.β123Updated 11 months ago
- Theorem Proving in Lean 4β191Updated this week
- Lean documentation authoring toolβ180Updated this week
- A Lean file formatterβ68Updated 2 years ago
- Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.β296Updated last year
- An introduction to theorem proving in Lean for the impatient.β210Updated last month
- LaTeX code for a paper on lean's type theoryβ137Updated 2 years ago
- The "batteries included" extended library for the Lean programming language and theorem proverβ311Updated this week
- Files associated with the course Interactive Theorem Proving at LMU SoSe 2024β62Updated 10 months ago
- Logic and Mechanized Reasoningβ104Updated 4 months ago
- White-box automation for Lean 4β275Updated this week
- An experimental proof assistant based on a type theory for synthetic β-categories.β233Updated 3 months ago
- Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) forβ¦β115Updated 2 months ago
- HoTTEST Summer School materialsβ299Updated 3 weeks ago
- A collection of tools for writing technical documents that mix Coq code and prose.β263Updated 4 months ago
- plasTeX plugin to build formalization blueprints.β220Updated last month
- Some Lean tutorialsβ183Updated last year