A project to digitalise results from physics into Lean.
-
Updated
Dec 16, 2025 - Lean
#
theorem-proving
Here are 36 public repositories matching this topic...
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
dependent-types theorem-proving program-synthesis formal-methods theorem-prover automated-reasoning dependent-type-theory lean4
-
Updated
Dec 15, 2025 - Lean
コード例で学ぶ Lean 言語
-
Updated
Dec 13, 2025 - Lean
(Mirror) A Machine-to-Machine Interaction System for Lean 4
-
Updated
Dec 12, 2025 - Lean
Extracting the semantics of Noir to Lean for formal verification
-
Updated
Dec 15, 2025 - Lean
Step-by-step small or medium-sized projects in Lean
-
Updated
Dec 3, 2025 - Lean
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
-
Updated
Nov 25, 2025 - Lean
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
dependent-types theorem-proving program-synthesis formal-methods theorem-prover automated-reasoning lean4
-
Updated
Nov 17, 2025 - Lean
Formal verification of GT-SMDN framework in Lean 4. 53 theorems formalised, 28 complete proofs. Companion to 'Protecting Critical Infrastructure' book.
theorem-proving cybersecurity game-theory formal-methods risk-assessment formal-verification critical-infrastructure lean4
-
Updated
Nov 17, 2025 - Lean
A Lean 4 eDSL for writing declarative, correct-by-construction packing lists for user defined expeditions (e.g. walking the Camino, hiking the CDT, dressing for a wedding)
-
Updated
Sep 21, 2025 - Lean
Miller–Rabin primality test in Lean
-
Updated
Dec 15, 2025 - Lean
Lean4 is a purely functional programming language based on the calculus of constructions with inductive types. Formal verification of claims are expressed in precise mathematical terms.
functional-programming theorem-proving mathematics proof-assistant calculus-of-constructions formal-verification inductive-logic-programming lean4
-
Updated
Sep 5, 2025 - Lean
A repository for studying and implementing Lean theorems, focusing on mathematical and philosophical concepts.
topology geometry theorem-proving mathematics lean formal-verification real-analysis euclidean-geometry theorem-provings lean4 philosophical-logic philosophical-mathematics
-
Updated
Jun 2, 2025 - Lean
Formalization projects for the Foundation of Software course at EPFL
-
Updated
May 21, 2025 - Lean
This project aims to formalize some concepts of Automata Theory and Parsing into Lean4 Theorem Prover. This was a course project for the course 'Proofs and Programs' offered by Prof Siddhartha Gadgil at IISc, Spring 2025.
-
Updated
May 5, 2025 - Lean
This repository holds exercises and solutions for the Lean for the Curious Mathematician 2023 (LftCM2023) workshop. Focused on formal mathematics with Lean 4, it provides a hands-on learning experience based on the "Mathematics in Lean" book. Updated in October 2024, it includes solutions and resources for exploring proofs and formal logic.
-
Updated
Oct 26, 2024 - Lean
Lean 3's obsolete mathematical components library: please use mathlib4
-
Updated
Jun 28, 2024 - Lean
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
-
Updated
Apr 8, 2024 - Lean
Lean Subtypes that have Super powers
-
Updated
Oct 31, 2023 - Lean
Improve this page
Add a description, image, and links to the theorem-proving topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the theorem-proving topic, visit your repo's landing page and select "manage topics."