GitHub topics: theorem-proving
chasenorman/CanonicalLean
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Language: Lean - Size: 8.15 MB - Last synced at: about 9 hours ago - Pushed at: about 11 hours ago - Stars: 85 - Forks: 7
RvnKali/Prime-Numbers
# Prime-Numbers Web AppThis web app helps users explore prime numbers through features like checking primality and generating sequences. With clear visuals and step-by-step explanations, it makes understanding prime numbers simple and engaging. 🐙✨
Language: HTML - Size: 21.5 KB - Last synced at: about 14 hours ago - Pushed at: about 16 hours ago - Stars: 0 - Forks: 0
FStarLang/FStar
A Proof-oriented Programming Language
Language: F* - Size: 755 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 2,894 - Forks: 243
MathewJHouser/Lean4-Code-Portfolio
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.
Language: Lean - Size: 56.6 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 0 - Forks: 0
reilabs/lampe
Extracting the semantics of Noir to Lean for formal verification
Language: Lean - Size: 3.25 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 34 - Forks: 4
CakeML/cakeml
CakeML: A Verified Implementation of ML
Language: Standard ML - Size: 125 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1,076 - Forks: 90
augustepoiroux/LeanInteract
LeanInteract: A Python Interface for Lean 4
Language: Python - Size: 2.33 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 51 - Forks: 8
hanwenzhu/miller-rabin
Miller–Rabin primality test in Lean
Language: Lean - Size: 129 KB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 6 - Forks: 0
Morphic-Symplexis/morphic-symplexis
A framework for formalizing systems, theories and metatheories in Lean and Rocq.
Size: 16.6 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 1 - Forks: 0
HEPLean/PhysLean
A project to digitalise results from physics into Lean.
Language: Lean - Size: 7.81 MB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 335 - Forks: 38
acl2/acl2
ACL2 System and Books as Maintained by the Community
Language: Common Lisp - Size: 1.41 GB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 404 - Forks: 117
leanprover-community/mathlib3 📦
Lean 3's obsolete mathematical components library: please use mathlib4
Language: Lean - Size: 213 MB - Last synced at: 5 days ago - Pushed at: about 1 year ago - Stars: 1,667 - Forks: 292
rocq-prover/rocq
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Language: OCaml - Size: 198 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 5,191 - Forks: 691
pitmonticone/LeanProject
A template for blueprint-driven formalization projects in Lean.
Language: Python - Size: 156 KB - Last synced at: 4 days ago - Pushed at: 20 days ago - Stars: 70 - Forks: 8
HOL-Theorem-Prover/HOL
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
Language: Standard ML - Size: 122 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 680 - Forks: 157
leoprover/Leo-III
An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
Language: Scala - Size: 34.4 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 49 - Forks: 10
lean-dojo/LeanDojoWebsite
Code for LeanDojo's website
Language: JavaScript - Size: 73.7 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 8 - Forks: 3
microsoft/DSP-Plus
Implementation and subsequent optimization for "Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models"
Language: Python - Size: 1.32 MB - Last synced at: 5 days ago - Pushed at: 3 months ago - Stars: 20 - Forks: 2
philzook58/knuckledragger
A Low Barrier Proof Assistant
Language: Python - Size: 8.53 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 124 - Forks: 7
leanprover/lean3 📦
Lean Theorem Prover
Language: C++ - Size: 50.3 MB - Last synced at: 1 day ago - Pushed at: almost 2 years ago - Stars: 2,153 - Forks: 220
taimoorzaeem/pl-stuff
PL Theory, Research and Implementation
Language: Racket - Size: 138 KB - Last synced at: 5 days ago - Pushed at: 9 days ago - Stars: 1 - Forks: 0
stanford-centaur/PyPantograph
A Machine-to-Machine Interaction System for Lean 4.
Language: Python - Size: 47 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 109 - Forks: 23
leanprover/Pantograph
(Mirror) A Machine-to-Machine Interaction System for Lean 4
Language: Lean - Size: 1.4 MB - Last synced at: 6 days ago - Pushed at: 8 days ago - Stars: 32 - Forks: 4
philzook58/Knuckledragger.jl
Julia Semi-Automated Proof Assistant
Language: Julia - Size: 6.84 KB - Last synced at: 3 days ago - Pushed at: 20 days ago - Stars: 5 - Forks: 1
leoprover/tptp-utils
Library for TPTP-related utility services
Language: Scala - Size: 1.39 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 4 - Forks: 0
coq-tactician/coq-tactician-api
An API for interfacing with Coq through Tactician by external agents
Language: Python - Size: 1.2 MB - Last synced at: 4 days ago - Pushed at: 2 months ago - Stars: 3 - Forks: 4
newca12/awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Size: 323 KB - Last synced at: 8 days ago - Pushed at: 15 days ago - Stars: 354 - Forks: 11
fritzo/pomagma
Inference engine for extensional untyped λ-calculus
Language: C++ - Size: 9.57 MB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 4 - Forks: 0
HOLMS-lib/HOLMS
HOL-Light Library for Modal Systems
Language: OCaml - Size: 333 KB - Last synced at: 14 days ago - Pushed at: 15 days ago - Stars: 2 - Forks: 0
vishallama/mathematics_in_lean Fork of leanprover-community/mathematics_in_lean
The user home repository for the Mathematics in Lean tutorial.
Language: HTML - Size: 49.8 MB - Last synced at: 14 days ago - Pushed at: 15 days ago - Stars: 0 - Forks: 0
lupantech/ineqmath
Solving Inequality Proofs with Large Language Models.
Language: Python - Size: 13.4 MB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 42 - Forks: 7
chasenorman/Canonical
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
Language: Lean - Size: 200 KB - Last synced at: 22 days ago - Pushed at: 22 days ago - Stars: 64 - Forks: 4
lean-dojo/LeanDojo
Tool for data extraction and interacting with Lean programmatically.
Language: Python - Size: 2.13 MB - Last synced at: 21 days ago - Pushed at: 3 months ago - Stars: 695 - Forks: 111
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Language: C++ - Size: 1.25 MB - Last synced at: 24 days ago - Pushed at: 24 days ago - Stars: 1,147 - Forks: 108
vvulpes0/Language-Toolkit-2
A set of tools for analyzing languages via logic and automata
Language: Haskell - Size: 2.01 MB - Last synced at: 24 days ago - Pushed at: 24 days ago - Stars: 23 - Forks: 0
Gbury/dolmen
Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
Language: OCaml - Size: 11.8 MB - Last synced at: 10 days ago - Pushed at: 25 days ago - Stars: 88 - Forks: 20
binghe/HOL Fork of HOL-Theorem-Prover/HOL
Forked sources of HOL4 (no cv_compute, etc.)
Language: Standard ML - Size: 130 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 7 - Forks: 2
tobias-rothmann/Polynomial-Commitment-Schemes
Formalizing Polynomial Commitment Schemes in the Interactive Theorem Prover Isabelle.
Language: Isabelle - Size: 4.3 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 10 - Forks: 0
stefanutti/maps-coloring-python
Four color theorem, Guthrie, Kempe, Tait and other people and stuff
Language: Python - Size: 29.1 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 10 - Forks: 4
thery/coqprime
Prime numbers for Coq
Language: Rocq Prover - Size: 13.4 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 42 - Forks: 18
OolonColoophid/bakerStreet
A natural deduction helper for macOS
Language: Swift - Size: 46.1 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 2 - Forks: 0
anqur/TinyLean
Tiny theorem prover with syntax like Lean 4 in <1K LOC
Language: Python - Size: 192 KB - Last synced at: about 6 hours ago - Pushed at: about 2 months ago - Stars: 64 - Forks: 2
AthenaFoundation/athena
Athena is a modern, practical language for proof engineering & natural deduction.
Language: Standard ML - Size: 12.7 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 73 - Forks: 4
coq-tactician/coq-tactician
A Seamless, Interactive Tactic Learner and Prover for Coq
Language: OCaml - Size: 2.2 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 74 - Forks: 25
gapt/gapt
GAPT: General Architecture for Proof Theory
Language: Scala - Size: 182 MB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 101 - Forks: 19
lean-dojo/ReProver
Retrieval-Augmented Theorem Provers for Lean
Language: Python - Size: 1.66 MB - Last synced at: about 2 months ago - Pushed at: 7 months ago - Stars: 284 - Forks: 60
wizard7377/SHIFT
Lamed calculus
Language: Haskell - Size: 2.49 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0
crisperdue/practical-logic
Code resources from John Harrison's "Handbook of Practical Logic and Automated Reasoning"
Language: OCaml - Size: 299 KB - Last synced at: 5 days ago - Pushed at: over 4 years ago - Stars: 8 - Forks: 1
uuverifiers/ostrich
An SMT Solver for string constraints
Language: Scala - Size: 232 MB - Last synced at: about 1 hour ago - Pushed at: 2 months ago - Stars: 39 - Forks: 8
brightlikethelight/proof-sketcher
📐 Natural language explanations of Lean 4 theorems | MathJax 4.0 rendering • Batch processing • Mathematical notation | Formal verification accessibility
Language: Python - Size: 7.5 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0
brightlikethelight/simpulse
🔧 Evidence-based Lean 4 simp optimization using real diagnostic data | Performance validation with measurable results | First evidence-based approach
Language: Python - Size: 6.28 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0
Seagat2011/Anthropic-Claude-Mathematical-Proof-Solver-
An elegant Anthropic Claude designed Mathematical Proof Solver, written in Javascript, HTML, and CSS.
Language: HTML - Size: 229 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 1
thery/minirubik
Solving the mini Rubik (2x2) in Coq
Language: Rocq Prover - Size: 198 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 5 - Forks: 0
cheuktingli/psitip
Python Symbolic Information Theoretic Inequality Prover
Language: Python - Size: 3.31 MB - Last synced at: 22 days ago - Pushed at: 3 months ago - Stars: 43 - Forks: 8
kovvalsky/LangPro
Tableau-based Theorem Prover for Natural Logic and Language
Language: Prolog - Size: 26.4 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 116 - Forks: 13
Inferara/inferara.com
Inferara official website
Language: HTML - Size: 2.13 MB - Last synced at: 23 days ago - Pushed at: 23 days ago - Stars: 1 - Forks: 2
joewatt95/CVM
Code repository for the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant"
Language: Isabelle - Size: 2.06 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 2 - Forks: 0
Mk9207/Constructive-Unified-Proof-Principle-
A compositional theory that unifies the proof of unsolved problems, AI structure, medical control, and physical modeling using a single constructive function C(x). 単一の構成関数C(x)により、未解決問題、AI構造、医療制御、物理モデルを統一的に証明・構成する理論です。
Size: 0 Bytes - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
dominique-unruh/scala-isabelle
A Scala library for controlling/interacting with Isabelle
Language: Scala - Size: 1.22 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 40 - Forks: 9
yakuza8/first-order-predicate-logic-theorem-prover
Autonomous Theorem Prover for First Order Predicate Logic
Language: Python - Size: 104 KB - Last synced at: about 2 months ago - Pushed at: about 5 years ago - Stars: 11 - Forks: 4
nyuichi/shari
A proof assistant based on the internal language of topos with NNO (intuitionistic higher-order arithmetic)
Language: Rust - Size: 5.72 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 5 - Forks: 0
Hifza-Khalid/FormalMethodsInSE
🔍A deep dive into Formal Methods in Software Engineering 📜—exploring automata, logic, verification, and specification techniques to ensure software correctness and reliability.
Language: Python - Size: 769 KB - Last synced at: about 2 months ago - Pushed at: 3 months ago - Stars: 4 - Forks: 0
evhub/pyprover
Resolution theorem proving for predicate logic in pure Python.
Language: Python - Size: 344 KB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 95 - Forks: 10
HxHippy/Beardicus-Theorem
This repository contains the code, data generation scripts, and documentation for a computational study exploring the relationships between the cuteness level of anime profile pictures, the beard prominence of users, and the probability that a user is actually a medieval fantasy dwarf.
Language: Python - Size: 337 KB - Last synced at: 3 months ago - Pushed at: 7 months ago - Stars: 1 - Forks: 0
johnyf/tool_lists
Links to tools by subject
Size: 63.5 KB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 375 - Forks: 83
chanind/tensor-theorem-prover
First-order logic theorem prover supporting unification with approximate vector similarity
Language: Rust - Size: 3.16 MB - Last synced at: 2 days ago - Pushed at: over 2 years ago - Stars: 12 - Forks: 1
leoprover/ask
Stand-alone Skolemizer for TPTP formulas
Language: Scala - Size: 569 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
princeton-vl/CoqGym
A Learning Environment for Theorem Proving with the Coq proof assistant
Language: Coq - Size: 32 MB - Last synced at: 3 months ago - Pushed at: about 2 years ago - Stars: 401 - Forks: 51
shilangyu/foundations_of_software_projects
Formalization projects for the Foundation of Software course at EPFL
Language: Lean - Size: 49.8 KB - Last synced at: 15 days ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0
thery/mathcomp-extra
Extra contribution for mathcomp
Language: Coq - Size: 545 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 5 - Forks: 2
thery/Plouffe
Computing Pi decimal using Plouffe Formula in Coq
Language: Coq - Size: 75.2 KB - Last synced at: 30 days ago - Pushed at: 4 months ago - Stars: 6 - Forks: 1
thery/EdwardsEllipticCurve
Group Law for Elliptic Curves according to Tom Hales
Language: Coq - Size: 280 KB - Last synced at: 3 months ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0
nikolashn/lichen
Set theoretic programming language
Language: D - Size: 93.8 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 2 - Forks: 0
sean-lamont/bait
Language: Standard ML - Size: 81.4 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 5 - Forks: 2
thery/robbins
Proof in Coq that all Robbins algebras are Boolean algebras
Language: Coq - Size: 34.2 KB - Last synced at: 2 months ago - Pushed at: 4 months ago - Stars: 3 - Forks: 1
NaveenMaurya749/AutomataLean
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.
Language: Lean - Size: 18.6 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0
loganrjmurphy/LeanEuclid
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Language: Lean - Size: 3.57 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 98 - Forks: 8
math-o-matic/math-o-matic
Computerized proof system on the web
Language: TypeScript - Size: 5.62 MB - Last synced at: 29 days ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 0
fadoss/maude2lean
Maude to Lean translator
Language: Lean - Size: 176 KB - Last synced at: 2 days ago - Pushed at: about 1 year ago - Stars: 6 - Forks: 0
MarisaKirisame/first_order_logic_prover
Language: C++ - Size: 338 KB - Last synced at: 5 days ago - Pushed at: over 7 years ago - Stars: 59 - Forks: 9
idris-hackers/software-foundations
Software Foundations in Idris
Language: Idris - Size: 4.25 MB - Last synced at: 4 months ago - Pushed at: over 6 years ago - Stars: 455 - Forks: 34
DominicPM/supervisionary
Supervisionary: a proof-checking system for HOL
Language: Rust - Size: 4.84 MB - Last synced at: 4 months ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0
binghe/HOL-Probability
Measure, Lebesgue and Probability Theory for HOL4 (leftovers)
Language: Standard ML - Size: 3.45 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 1
lean-dojo/LeanDojoChatGPT
ChatGPT plugin for theorem proving in Lean
Language: Python - Size: 344 KB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 118 - Forks: 14
bor0/gidti
Book: Introduction to Dependent Types with Idris
Size: 10.9 MB - Last synced at: 4 months ago - Pushed at: over 2 years ago - Stars: 78 - Forks: 4
fsestini/zsyntax
Automated theorem prover for a linear logic-based calculus for molecular biology.
Language: Haskell - Size: 709 KB - Last synced at: 19 days ago - Pushed at: about 2 years ago - Stars: 12 - Forks: 0
yurrriq/tdd-with-idris
:book: Working through Type-Driven Development with Idris
Language: Idris - Size: 221 KB - Last synced at: about 1 month ago - Pushed at: over 8 years ago - Stars: 2 - Forks: 1
jonaprieto/agda-prop 📦
A Library for Classical Propositional Logic in Agda
Language: Agda - Size: 442 KB - Last synced at: about 2 months ago - Pushed at: almost 6 years ago - Stars: 16 - Forks: 1
mister-walter/acl2s-docker
A Docker image for the ACL2 Sedan extension to the ACL2 theorem proving system
Language: Makefile - Size: 11.7 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0
mister-walter/acl2-docker
A Docker image for the ACL2 theorem proving system and books
Language: Dockerfile - Size: 47.9 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 3 - Forks: 0
gpoesia/peano
An environment for learning formal mathematical reasoning from scratch
Language: Python - Size: 349 KB - Last synced at: 4 months ago - Pushed at: about 1 year ago - Stars: 66 - Forks: 7
EugeneLoy/coq_jupyter
Jupyter kernel for Coq
Language: Python - Size: 414 KB - Last synced at: 18 days ago - Pushed at: about 1 year ago - Stars: 95 - Forks: 8
wellecks/llmstep
llmstep: [L]LM proofstep suggestions in Lean 4.
Language: Python - Size: 1.56 MB - Last synced at: 5 months ago - Pushed at: almost 2 years ago - Stars: 130 - Forks: 15
leoprover/scala-tptp-parser
A parser for the TPTP logic languages for automated theorem proving written in Scala
Language: Scala - Size: 168 KB - Last synced at: 4 months ago - Pushed at: 6 months ago - Stars: 6 - Forks: 6
hengxin/tlaps-examples
Examples for TLAPS (TLA+ Proof System)
Language: TeX - Size: 4.76 MB - Last synced at: 12 days ago - Pushed at: over 5 years ago - Stars: 14 - Forks: 6
Edward-Ji/LogicSolver
Step-by-step proof for equivalence in propositional logic and ND prover for first-order logic.
Language: Python - Size: 57.6 KB - Last synced at: 3 months ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
unprosaiclabyrinth/incsum
Prove spec for a program that increases a list and sums it in parallel (Final project, CS 472, Spring 2024 @ UIC).
Language: Coq - Size: 5.86 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0
LS-Lab/Verified-Neural-Highway-Control
Verification of Autonomous Neural Car Control with KeYmaera X
Language: Jupyter Notebook - Size: 34.1 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0
pro465/nyaya
proof language based on https://en.wikipedia.org/wiki/Sequent_calculus and https://us.metamath.org/.
Language: Rust - Size: 46.9 KB - Last synced at: 4 months ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0
gebner/trepplein
Lean type-checker written in Scala.
Language: Scala - Size: 118 KB - Last synced at: 5 months ago - Pushed at: over 3 years ago - Stars: 35 - Forks: 2
