Topic: "theorem-proving"
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: 195 MB - Last synced at: 7 days ago - Pushed at: 9 days ago - Stars: 5,030 - Forks: 679
FStarLang/FStar
A Proof-oriented Programming Language
Language: F* - Size: 752 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 2,826 - Forks: 239
leanprover/lean3 📦
Lean Theorem Prover
Language: C++ - Size: 50.3 MB - Last synced at: 9 days ago - Pushed at: over 1 year ago - Stars: 2,150 - Forks: 217
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: 10 months ago - Stars: 1,663 - Forks: 294
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Language: C++ - Size: 1.22 MB - Last synced at: 10 days ago - Pushed at: 11 days ago - Stars: 1,072 - Forks: 99
CakeML/cakeml
CakeML: A Verified Implementation of ML
Language: Standard ML - Size: 118 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 1,022 - Forks: 87
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: 117 MB - Last synced at: 10 days ago - Pushed at: 11 days ago - Stars: 656 - Forks: 148
lean-dojo/LeanDojo
Tool for data extraction and interacting with Lean programmatically.
Language: Python - Size: 2.23 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 647 - Forks: 101
idris-hackers/software-foundations
Software Foundations in Idris
Language: Idris - Size: 4.25 MB - Last synced at: 6 months ago - Pushed at: almost 6 years ago - Stars: 452 - Forks: 34
princeton-vl/CoqGym
A Learning Environment for Theorem Proving with the Coq proof assistant
Language: Coq - Size: 32 MB - Last synced at: 22 days ago - Pushed at: almost 2 years ago - Stars: 397 - Forks: 51
dselsam/certigrad
Bug-free machine learning on stochastic computation graphs
Language: Lean - Size: 289 KB - Last synced at: about 1 month ago - Pushed at: about 6 years ago - Stars: 390 - Forks: 35
acl2/acl2
ACL2 System and Books as Maintained by the Community
Language: Common Lisp - Size: 1.36 GB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 385 - Forks: 107
johnyf/tool_lists
Links to tools by subject
Size: 63.5 KB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 375 - Forks: 83
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: 312 KB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 330 - Forks: 11
HEPLean/PhysLean
A project to digitalise results from physics into Lean.
Language: Lean - Size: 4.92 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 206 - Forks: 18
siddhartha-gadgil/ProvingGround
Proving Ground: Tools for Automated Mathematics
Language: Jupyter Notebook - Size: 435 MB - Last synced at: 5 months ago - Pushed at: over 3 years ago - Stars: 203 - Forks: 38
lean-dojo/ReProver
Retrieval-Augmented Theorem Provers for Lean
Language: Python - Size: 1.65 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 158 - Forks: 27
wellecks/llmstep
llmstep: [L]LM proofstep suggestions in Lean 4.
Language: Python - Size: 1.56 MB - Last synced at: 21 days ago - Pushed at: over 1 year ago - Stars: 130 - Forks: 15
lean-dojo/LeanDojoChatGPT
ChatGPT plugin for theorem proving in Lean
Language: Python - Size: 344 KB - Last synced at: 7 days ago - Pushed at: about 1 year ago - Stars: 118 - Forks: 14
kovvalsky/LangPro
Tableau-based Theorem Prover for Natural Logic and Language
Language: Prolog - Size: 26.3 MB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 117 - Forks: 12
philzook58/knuckledragger
A Low Barrier Proof Assistant
Language: Python - Size: 7.45 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 108 - Forks: 5
gapt/gapt
GAPT: General Architecture for Proof Theory
Language: Scala - Size: 182 MB - Last synced at: 5 days ago - Pushed at: 17 days ago - Stars: 98 - Forks: 18
EugeneLoy/coq_jupyter
Jupyter kernel for Coq
Language: Python - Size: 414 KB - Last synced at: about 1 month ago - Pushed at: 8 months ago - Stars: 96 - Forks: 8
evhub/pyprover
Resolution theorem proving for predicate logic in pure Python.
Language: Python - Size: 344 KB - Last synced at: 27 days ago - Pushed at: over 1 year ago - Stars: 93 - Forks: 10
Gbury/dolmen
Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
Language: OCaml - Size: 10.8 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 85 - Forks: 18
binghe/informatica-public
Public code developed during my MSc study at University of Bologna
Language: Standard ML - Size: 25.7 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 78 - Forks: 7
loganrjmurphy/LeanEuclid
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Language: Lean - Size: 3.59 MB - Last synced at: 5 months ago - Pushed at: 11 months ago - Stars: 76 - Forks: 5
bor0/gidti
Book: Introduction to Dependent Types with Idris
Size: 10.9 MB - Last synced at: 2 months ago - Pushed at: about 2 years ago - Stars: 76 - Forks: 4
stanford-centaur/PyPantograph
A Machine-to-Machine Interaction System for Lean 4.
Language: Python - Size: 46.8 MB - Last synced at: 1 day ago - Pushed at: 4 days ago - Stars: 73 - Forks: 17
ml4tp/gamepad
A Learning Environment for Theorem Proving
Language: Coq - Size: 53.8 MB - Last synced at: 21 days ago - Pushed at: almost 3 years ago - Stars: 73 - Forks: 15
AthenaFoundation/athena
Athena is a modern, practical language for proof engineering & natural deduction.
Language: Standard ML - Size: 12.6 MB - Last synced at: 8 days ago - Pushed at: 9 days ago - Stars: 71 - Forks: 4
coq-tactician/coq-tactician
A Seamless, Interactive Tactic Learner and Prover for Coq
Language: OCaml - Size: 2.24 MB - Last synced at: 18 days ago - Pushed at: 24 days ago - Stars: 64 - Forks: 21
choukh/Set-Theory
A formalization of the textbook Elements of Set Theory
Language: Coq - Size: 3.79 MB - Last synced at: 6 months ago - Pushed at: over 3 years ago - Stars: 59 - Forks: 4
MarisaKirisame/first_order_logic_prover
Language: C++ - Size: 338 KB - Last synced at: 13 days ago - Pushed at: about 7 years ago - Stars: 58 - Forks: 9
salmans/rusty-razor
Razor is a tool for constructing finite models for first-order theories
Language: Rust - Size: 1.28 MB - Last synced at: 15 days ago - Pushed at: over 2 years ago - Stars: 55 - Forks: 1
pitmonticone/LeanProject
Template for blueprint-driven formalization projects in Lean.
Language: Python - Size: 129 KB - Last synced at: about 19 hours ago - Pushed at: 13 days ago - Stars: 48 - Forks: 4
tlaplus-workshops/ewd998
Distributed termination detection on a ring, due to Shmuel Safra:
Language: TLA - Size: 1.95 MB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 46 - Forks: 47
leoprover/Leo-III
An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
Language: Scala - Size: 34 MB - Last synced at: 5 days ago - Pushed at: 23 days ago - Stars: 45 - Forks: 10
choukh/Baby-Set-Theory
Coq集合论中文教程
Language: Coq - Size: 401 KB - Last synced at: 15 days ago - Pushed at: over 3 years ago - Stars: 44 - Forks: 3
lemmy/ewd998 📦
Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF
Language: TLA - Size: 1.61 MB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 41 - Forks: 12
gpoesia/peano
An environment for learning formal mathematical reasoning from scratch
Language: Python - Size: 346 KB - Last synced at: 11 months ago - Pushed at: 12 months ago - Stars: 40 - Forks: 2
uuverifiers/ostrich
An SMT Solver for string constraints
Language: Scala - Size: 232 MB - Last synced at: 6 days ago - Pushed at: about 1 month ago - Stars: 38 - Forks: 8
Eleanor-H/MUSTARD
Code & data for ICLR 2024 spotlight paper: 🍯MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
Language: C++ - Size: 21 MB - Last synced at: 3 months ago - Pushed at: 11 months ago - Stars: 38 - Forks: 1
thery/coqprime
Prime numbers for Coq
Language: Coq - Size: 13 MB - Last synced at: 15 days ago - Pushed at: 3 months ago - Stars: 37 - Forks: 18
cheuktingli/psitip
Python Symbolic Information Theoretic Inequality Prover
Language: Python - Size: 2.56 MB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 37 - Forks: 8
gebner/trepplein
Lean type-checker written in Scala.
Language: Scala - Size: 118 KB - Last synced at: 20 days ago - Pushed at: about 3 years ago - Stars: 35 - Forks: 2
dominique-unruh/scala-isabelle
A Scala library for controlling/interacting with Isabelle
Language: Scala - Size: 1.21 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 32 - Forks: 8
llee454/functional-algebra
This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
Language: Coq - Size: 1.95 MB - Last synced at: 9 months ago - Pushed at: about 6 years ago - Stars: 28 - Forks: 2
ai4reason/Prover9
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
Language: C - Size: 1.81 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 27 - Forks: 8
Gbury/archsat
A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.
Language: OCaml - Size: 2.14 MB - Last synced at: 5 days ago - Pushed at: almost 2 years ago - Stars: 27 - Forks: 5
reilabs/lampe
Extracting the semantics of Noir to Lean for formal verification
Language: Lean - Size: 2.76 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 26 - Forks: 2
vvulpes0/Language-Toolkit-2
A set of tools for analyzing languages via logic and automata
Language: Haskell - Size: 1.93 MB - Last synced at: 5 days ago - Pushed at: 6 days ago - Stars: 24 - Forks: 0
anqur/TinyLean
Tiny theorem prover with syntax like Lean 4 in <1K LOC
Language: Python - Size: 285 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 23 - Forks: 0
iwilare/church-rosser
A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses the infrastructure for λ-terms and substitutions provided by the PLFA book
Language: Agda - Size: 70.3 KB - Last synced at: 9 months ago - Pushed at: over 2 years ago - Stars: 22 - Forks: 1
lenianiva/Pantograph
(Mirror) A Machine-to-Machine Interaction System for Lean 4
Language: Lean - Size: 902 KB - Last synced at: 1 day ago - Pushed at: 7 days ago - Stars: 20 - Forks: 3
Coq-Polyhedra/Coq-Polyhedra
Formalizing convex polyhedra in Coq
Language: Coq - Size: 116 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 20 - Forks: 4
mgrabovsky/fm-notes
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Language: Coq - Size: 218 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 20 - Forks: 2
fritzo/pomagma
An inference engine for extensional untyped λ-calculus
Language: C++ - Size: 7.99 MB - Last synced at: 15 days ago - Pushed at: about 2 years ago - Stars: 17 - Forks: 2
RichardMoot/LinearOne
LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.
Language: Prolog - Size: 563 KB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 16 - Forks: 2
jonaprieto/agda-prop
A Library for Classical Propositional Logic in Agda
Language: Agda - Size: 442 KB - Last synced at: 22 days ago - Pushed at: over 5 years ago - Stars: 16 - Forks: 1
catseye/Philomath
MIRROR of https://codeberg.org/catseye/Philomath : An LCF-style theorem prover written in C89 (a.k.a ANSI C)
Language: C - Size: 51.8 KB - Last synced at: 18 days ago - Pushed at: over 1 year ago - Stars: 14 - Forks: 2
hengxin/tlaps-examples
Examples for TLAPS (TLA+ Proof System)
Language: TeX - Size: 4.76 MB - Last synced at: 2 months ago - Pushed at: almost 5 years ago - Stars: 13 - Forks: 6
hengxin/tlaplus-at-nju-disalg
Learning [Lamport's TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).
Language: TeX - Size: 231 MB - Last synced at: 2 months ago - Pushed at: about 3 years ago - Stars: 12 - Forks: 7
fsestini/zsyntax
Automated theorem prover for a linear logic-based calculus for molecular biology.
Language: Haskell - Size: 709 KB - Last synced at: about 1 month ago - Pushed at: almost 2 years ago - Stars: 11 - Forks: 0
ice1k/Theorems
:globe_with_meridians: Theorems that rule this multiverse
Language: Agda - Size: 76.2 KB - Last synced at: 5 months ago - Pushed at: over 6 years ago - Stars: 11 - Forks: 2
chasenorman/Canonical
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
Language: Lean - Size: 81.1 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 10 - Forks: 1
stefanutti/maps-coloring-python
Four color theorem, Guthrie, Kempe, Tait and other people and stuff
Language: Python - Size: 26.8 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 10 - Forks: 4
chanind/tensor-theorem-prover
First-order logic theorem prover supporting unification with approximate vector similarity
Language: Rust - Size: 3.16 MB - Last synced at: 13 days ago - Pushed at: about 2 years ago - Stars: 10 - Forks: 1
yakuza8/first-order-predicate-logic-theorem-prover
Autonomous Theorem Prover for First Order Predicate Logic
Language: Python - Size: 104 KB - Last synced at: 12 days ago - Pushed at: almost 5 years ago - Stars: 10 - Forks: 4
muraliadithya/mini-sygus
a constraint-based syntax-guided synthesis (SyGuS) engine
Language: Python - Size: 267 KB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 9 - Forks: 0
aztek/atp
Haskell interface to automated theorem provers
Language: Haskell - Size: 352 KB - Last synced at: 5 days ago - Pushed at: about 3 years ago - Stars: 9 - Forks: 0
lean-dojo/LeanDojoWebsite
Code for LeanDojo's website
Language: JavaScript - Size: 42.7 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 8 - Forks: 2
triska/presprover
Prove formulas of Presburger Arithmetic
Language: Prolog - Size: 34.2 KB - Last synced at: about 1 month ago - Pushed at: 7 months ago - Stars: 8 - Forks: 2
owings1/pytableaux
multi-logic proof generator
Language: Python - Size: 13 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 8 - Forks: 0
doofin/hott-examples
Homotopy type theory for theorem proving with univalence
Language: Agda - Size: 1.47 MB - Last synced at: 1 day ago - Pushed at: over 3 years ago - Stars: 8 - Forks: 0
binghe/HOL Fork of HOL-Theorem-Prover/HOL
Forked sources for HOL4 theorem-proving system (K15)
Language: Standard ML - Size: 120 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 7 - Forks: 2
potassco/anthem-1 📦
🎼 Translate answer set programs to first-order theorem prover language
Language: Rust - Size: 1.37 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 7 - Forks: 5
dtumad/lean-crypto-formalization
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
Language: Lean - Size: 2.13 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 7 - Forks: 0
Lolirofle/stuff-in-agda
Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.
Language: Agda - Size: 4.67 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 7 - Forks: 1
aztek/tptp
Parser and pretty printer for the TPTP language
Language: Haskell - Size: 1.49 MB - Last synced at: about 19 hours ago - Pushed at: over 3 years ago - Stars: 7 - Forks: 2
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: almost 4 years ago - Stars: 7 - Forks: 0
Lix0120/eudoxus
Formalise Eudoxus reals in lean and prove they form a complete Archimedean ordered field.
Language: Lean - Size: 123 KB - Last synced at: 5 months ago - Pushed at: about 4 years ago - Stars: 7 - Forks: 1
desi-ivanov/agda-regexp-automata
Formalization of Regular Languages in Agda: regular expressions, finite-state automata, proof of equivalence, proof of the pumping lemma.
Language: Agda - Size: 840 KB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 7 - Forks: 0
ml4tp/tcoq
Modification to Coq to record intermediate proof states encountered during a proof
Language: OCaml - Size: 65.9 MB - Last synced at: 14 days ago - Pushed at: almost 6 years ago - Stars: 7 - Forks: 2
LS-Lab/orbital
Orbital Library
Language: Java - Size: 4.7 MB - Last synced at: 9 months ago - Pushed at: about 8 years ago - Stars: 7 - Forks: 3
RichardMoot/Grail0
Grail0 is a bare-bones proof net theorem prover for multimodal categorial grammars producing natural deduction output
Language: Prolog - Size: 658 KB - Last synced at: about 2 years ago - Pushed at: over 9 years ago - Stars: 7 - Forks: 3
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: 27 days ago - Pushed at: about 1 month ago - Stars: 6 - Forks: 6
thery/Plouffe
Computing Pi decimal using Plouffe Formula in Coq
Language: Coq - Size: 56.6 KB - Last synced at: 20 days ago - Pushed at: 4 months ago - Stars: 6 - Forks: 1
math-o-matic/math-o-matic
Computerized proof system on the web
Language: TypeScript - Size: 5.62 MB - Last synced at: 9 months ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 0
cpressey/LCF-style-ND
Exposition of an LCF-style theorem prover for propositional logic in a Natural Deduction system
Size: 123 KB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 0
joewatt95/lambdacplus
A proof assistant based on the Calculus of Constructions
Language: JavaScript - Size: 33.7 MB - Last synced at: 11 months ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 1
jonaprieto/athena 📦
Translates Metis ATP proofs to the Agda code
Language: TeX - Size: 15.1 MB - Last synced at: about 1 year ago - Pushed at: about 5 years ago - Stars: 6 - Forks: 2
pfnet-research/chainer-formulanet
Chainer implementation of FormulaNet
Language: Python - Size: 7.98 MB - Last synced at: 14 days ago - Pushed at: about 5 years ago - Stars: 6 - Forks: 3
courses-at-nju-by-hfwei/problem-solving-class-coq
Rock on Coq for the Problem Solving Class at Nanjing University
Language: HTML - Size: 5.83 MB - Last synced at: 21 days ago - Pushed at: over 5 years ago - Stars: 6 - Forks: 7
sean-lamont/bait
Language: Standard ML - Size: 80.9 MB - Last synced at: 10 days ago - Pushed at: 11 days ago - Stars: 5 - Forks: 2
nyuichi/shari
A proof assistant based on the internal language of topos with NNO (intuitionistic higher-order arithmetic)
Language: Rust - Size: 5.12 MB - Last synced at: 14 days ago - Pushed at: about 1 month ago - Stars: 5 - Forks: 0
thery/mathcomp-extra
Extra contribution for mathcomp
Language: Coq - Size: 486 KB - Last synced at: 23 days ago - Pushed at: about 2 months ago - Stars: 5 - Forks: 2
fadoss/maude2lean
Maude to Lean translator
Language: Lean - Size: 176 KB - Last synced at: 14 days ago - Pushed at: 8 months ago - Stars: 5 - Forks: 0
hanwenzhu/primality-tests
Miller–Rabin primality test in Lean
Language: Lean - Size: 63.5 KB - Last synced at: 5 days ago - Pushed at: over 1 year ago - Stars: 5 - Forks: 0
rasheedja/LPPaver
An automated prover targeting problems that involve nonlinear real arithmetic.
Language: JavaScript - Size: 1.62 MB - Last synced at: 21 days ago - Pushed at: over 1 year ago - Stars: 5 - Forks: 0
