anqur/TinyLean

Tiny theorem prover with syntax like Lean 4 in <1K LOC

Language: Python - Size: 285 KB - Last synced at: about 11 hours ago - Pushed at: about 11 hours ago - Stars: 29 - Forks: 2

HEPLean/PhysLean

A project to digitalise results from physics into Lean.

Language: Lean - Size: 5.32 MB - Last synced at: about 13 hours ago - Pushed at: about 13 hours ago - Stars: 275 - Forks: 25

stanford-centaur/PyPantograph

A Machine-to-Machine Interaction System for Lean 4.

Language: Python - Size: 46.9 MB - Last synced at: 1 day ago - Pushed at: 5 days ago - Stars: 101 - Forks: 21

augustepoiroux/LeanInteract

LeanInteract: A Python Interface for Lean 4

Language: Python - Size: 307 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 35 - Forks: 6

leanprover/Pantograph

(Mirror) A Machine-to-Machine Interaction System for Lean 4

Language: Lean - Size: 1.01 MB - Last synced at: 1 day ago - Pushed at: 6 days ago - Stars: 27 - Forks: 3

CakeML/cakeml

CakeML: A Verified Implementation of ML

Language: Standard ML - Size: 119 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 1,058 - Forks: 88

philzook58/knuckledragger

A Low Barrier Proof Assistant

Language: Python - Size: 7.82 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 112 - Forks: 7

fritzo/pomagma

An inference engine for extensional untyped λ-calculus

Language: C++ - Size: 8.92 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 3 - 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 days ago - Pushed at: 3 days ago - Stars: 0 - Forks: 0

chasenorman/Canonical

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

Language: Lean - Size: 191 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 55 - Forks: 4

joewatt95/CVM

Code repository for the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant"

Language: Isabelle - Size: 2 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 1 - Forks: 0

thery/coqprime

Prime numbers for Coq

Language: Rocq Prover - Size: 13.4 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 39 - Forks: 18

reilabs/lampe

Extracting the semantics of Noir to Lean for formal verification

Language: Lean - Size: 2.52 MB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 32 - Forks: 4

pitmonticone/LeanProject

Template for blueprint-driven formalization projects in Lean.

Language: Python - Size: 136 KB - Last synced at: 4 days ago - Pushed at: 6 days ago - Stars: 57 - Forks: 8

uuverifiers/ostrich

An SMT Solver for string constraints

Language: Scala - Size: 232 MB - Last synced at: 3 days ago - Pushed at: 6 days ago - Stars: 39 - Forks: 8

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: 6 days ago - Pushed at: 6 days ago - Stars: 0 - Forks: 0

leoprover/Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics

Language: Scala - Size: 34 MB - Last synced at: about 23 hours ago - Pushed at: 6 days ago - Stars: 47 - Forks: 10

leanprover-community/mathlib3 📦

Lean 3's obsolete mathematical components library: please use mathlib4

Language: Lean - Size: 213 MB - Last synced at: 6 days ago - Pushed at: 12 months ago - Stars: 1,668 - Forks: 293

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: 196 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 5,133 - Forks: 685

acl2/acl2

ACL2 System and Books as Maintained by the Community

Language: Common Lisp - Size: 1.38 GB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 397 - Forks: 110

chasenorman/CanonicalLean

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

Language: Lean - Size: 8.83 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 75 - Forks: 4

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: 119 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 672 - Forks: 152

FStarLang/FStar

A Proof-oriented Programming Language

Language: F* - Size: 752 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 2,854 - Forks: 239

Inferara/inferara.com

Inferara official website

Language: HTML - Size: 949 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 1 - Forks: 2

dominique-unruh/scala-isabelle

A Scala library for controlling/interacting with Isabelle

Language: Scala - Size: 1.22 MB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 40 - Forks: 9

binghe/HOL Fork of HOL-Theorem-Prover/HOL

Forked sources of HOL4 (no cv_compute, etc.)

Language: Standard ML - Size: 125 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 6 - Forks: 2

leanprover/lean3 📦

Lean Theorem Prover

Language: C++ - Size: 50.3 MB - Last synced at: 12 days ago - Pushed at: over 1 year ago - Stars: 2,152 - Forks: 218

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: 12 days ago - Pushed at: 15 days 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: 14 days ago - Pushed at: 16 days ago - Stars: 4 - Forks: 0

lean-dojo/LeanDojo

Tool for data extraction and interacting with Lean programmatically.

Language: Python - Size: 2.26 MB - Last synced at: 16 days ago - Pushed at: 16 days ago - Stars: 670 - Forks: 106

OolonColoophid/bakerStreet

A natural deduction helper for macOS

Language: Swift - Size: 46.2 MB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 2 - Forks: 0

evhub/pyprover

Resolution theorem proving for predicate logic in pure Python.

Language: Python - Size: 344 KB - Last synced at: 16 days ago - Pushed at: over 1 year ago - Stars: 95 - Forks: 10

lean-dojo/LeanCopilot

LLMs as Copilots for Theorem Proving in Lean

Language: C++ - Size: 1.21 MB - Last synced at: 20 days ago - Pushed at: 20 days ago - Stars: 1,093 - Forks: 99

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: 13 days ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

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: 316 KB - Last synced at: 6 days ago - Pushed at: 24 days ago - Stars: 342 - Forks: 11

johnyf/tool_lists

Links to tools by subject

Size: 63.5 KB - Last synced at: 18 days 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: 11 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: 28 days ago - Pushed at: 28 days ago - Stars: 0 - Forks: 0

gapt/gapt

GAPT: General Architecture for Proof Theory

Language: Scala - Size: 182 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 100 - Forks: 19

princeton-vl/CoqGym

A Learning Environment for Theorem Proving with the Coq proof assistant

Language: Coq - Size: 32 MB - Last synced at: about 1 month ago - Pushed at: almost 2 years ago - Stars: 401 - Forks: 51

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: 3 days ago - Pushed at: about 1 month ago - Stars: 3 - Forks: 4

shilangyu/foundations_of_software_projects

Formalization projects for the Foundation of Software course at EPFL

Language: Lean - Size: 49.8 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - 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.3 MB - Last synced at: 8 days ago - Pushed at: about 1 month ago - Stars: 87 - Forks: 19

thery/mathcomp-extra

Extra contribution for mathcomp

Language: Coq - Size: 545 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 5 - Forks: 2

thery/Plouffe

Computing Pi decimal using Plouffe Formula in Coq

Language: Coq - Size: 75.2 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 6 - Forks: 1

thery/EdwardsEllipticCurve

Group Law for Elliptic Curves according to Tom Hales

Language: Coq - Size: 280 KB - Last synced at: 2 days ago - Pushed at: about 1 month ago - Stars: 1 - Forks: 0

nikolashn/lichen

Set theoretic programming language

Language: D - Size: 93.8 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 2 - Forks: 0

sean-lamont/bait

Language: Standard ML - Size: 81.4 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 5 - Forks: 2

kovvalsky/LangPro

Tableau-based Theorem Prover for Natural Logic and Language

Language: Prolog - Size: 26.4 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 116 - Forks: 12

thery/robbins

Proof in Coq that all Robbins algebras are Boolean algebras

Language: Coq - Size: 34.2 KB - Last synced at: 6 days ago - Pushed at: about 2 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: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

coq-tactician/coq-tactician

A Seamless, Interactive Tactic Learner and Prover for Coq

Language: OCaml - Size: 2.24 MB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 66 - Forks: 23

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: about 2 months ago - Pushed at: about 2 months ago - Stars: 98 - Forks: 8

idris-hackers/software-foundations

Software Foundations in Idris

Language: Idris - Size: 4.25 MB - Last synced at: about 2 months ago - Pushed at: about 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: about 2 months ago - Pushed at: about 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: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 1

lean-dojo/LeanDojoChatGPT

ChatGPT plugin for theorem proving in Lean

Language: Python - Size: 344 KB - Last synced at: 2 months ago - Pushed at: about 1 year ago - Stars: 118 - Forks: 14

bor0/gidti

Book: Introduction to Dependent Types with Idris

Size: 10.9 MB - Last synced at: about 1 month 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: 28 days ago - Pushed at: about 2 years ago - Stars: 12 - Forks: 0

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: 2 months ago - Pushed at: 2 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: 2 months ago - Pushed at: 2 months ago - Stars: 3 - Forks: 0

AthenaFoundation/athena

Athena is a modern, practical language for proof engineering & natural deduction.

Language: Standard ML - Size: 12.6 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 71 - Forks: 4

gpoesia/peano

An environment for learning formal mathematical reasoning from scratch

Language: Python - Size: 349 KB - Last synced at: about 2 months ago - Pushed at: 10 months ago - Stars: 66 - Forks: 7

EugeneLoy/coq_jupyter

Jupyter kernel for Coq

Language: Python - Size: 414 KB - Last synced at: 8 days ago - Pushed at: 10 months ago - Stars: 95 - Forks: 8

cheuktingli/psitip

Python Symbolic Information Theoretic Inequality Prover

Language: Python - Size: 2.56 MB - Last synced at: 16 days ago - Pushed at: over 1 year ago - Stars: 39 - Forks: 8

wellecks/llmstep

llmstep: [L]LM proofstep suggestions in Lean 4.

Language: Python - Size: 1.56 MB - Last synced at: 3 months ago - Pushed at: over 1 year 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: about 2 months ago - Pushed at: 3 months ago - Stars: 6 - Forks: 6

crisperdue/practical-logic

Code resources from John Harrison's "Handbook of Practical Logic and Automated Reasoning"

Language: OCaml - Size: 299 KB - Last synced at: about 19 hours ago - Pushed at: about 4 years ago - Stars: 7 - Forks: 1

fadoss/maude2lean

Maude to Lean translator

Language: Lean - Size: 176 KB - Last synced at: 2 months ago - Pushed at: 10 months ago - Stars: 5 - Forks: 0

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: 8 days 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: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

lean-dojo/LeanDojoWebsite

Code for LeanDojo's website

Language: JavaScript - Size: 42.7 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 8 - Forks: 2

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: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

Seagat2011/Anthropic-Claude-Mathematical-Proof-Solver-

An elegant Anthropic Claude designed Mathematical Proof Solver, written in Javascript, HTML, and CSS.

Language: JavaScript - Size: 190 KB - Last synced at: 3 months ago - Pushed at: 4 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: about 2 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: 3 months ago - Pushed at: over 3 years ago - Stars: 35 - Forks: 2

dselsam/certigrad

Bug-free machine learning on stochastic computation graphs

Language: Lean - Size: 289 KB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 390 - Forks: 35

HOLMS-lib/HOLMS

HOL-Light Library for Modal Systems

Language: OCaml - Size: 212 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 1 - 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: 4 months ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 0

aztek/atp

Haskell interface to automated theorem provers

Language: Haskell - Size: 352 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 9 - Forks: 0

ml4tp/gamepad

A Learning Environment for Theorem Proving

Language: Coq - Size: 53.8 MB - Last synced at: 3 months ago - Pushed at: about 3 years ago - Stars: 73 - Forks: 15

DmytroMitin/arend-exercises

Size: 3.91 KB - Last synced at: 4 months ago - Pushed at: over 6 years ago - Stars: 4 - Forks: 0

lukaszcz/hcpl

A prototypical proof checker and programming language based on illative combinatory logic

Language: OCaml - Size: 350 KB - Last synced at: 22 days ago - Pushed at: 10 months ago - Stars: 3 - Forks: 0

costowell/theorem-prover

Verify equation truth using a custom logical language

Language: Rust - Size: 51.8 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

taimoorzaeem/smart_contract_verification 📦

Formally Verifying Smart Contracts using Theorem Proving

Language: Standard ML - Size: 300 KB - Last synced at: 3 months ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

pfnet-research/chainer-formulanet

Chainer implementation of FormulaNet

Language: Python - Size: 7.98 MB - Last synced at: 2 months ago - Pushed at: over 5 years ago - Stars: 6 - Forks: 3

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: 5 months ago - Pushed at: about 1 year ago - Stars: 38 - Forks: 1

jonaprieto/agda-metis

Metis Prover Reasoning for Propositional Logic in Agda

Language: Agda - Size: 765 KB - Last synced at: 27 days ago - Pushed at: over 6 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: 3 months ago - Pushed at: over 5 years ago - Stars: 16 - Forks: 1

hengxin/tlaps-examples

Examples for TLAPS (TLA+ Proof System)

Language: TeX - Size: 4.76 MB - Last synced at: 4 months ago - Pushed at: about 5 years ago - Stars: 13 - Forks: 6

stefanutti/maps-coloring-python

Four color theorem, Guthrie, Kempe, Tait and other people and stuff

Language: Python - Size: 26.8 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 10 - Forks: 4

choukh/Baby-Set-Theory

Coq集合论中文教程

Language: Coq - Size: 401 KB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 44 - Forks: 3

triska/presprover

Prove formulas of Presburger Arithmetic

Language: Prolog - Size: 34.2 KB - Last synced at: 3 months ago - Pushed at: 9 months ago - Stars: 8 - Forks: 2

thery/minirubik

Solving the mini Rubik (2x2) in Coq

Language: Coq - Size: 165 KB - Last synced at: 3 months ago - Pushed at: 6 months ago - Stars: 4 - Forks: 0

MarisaKirisame/first_order_logic_prover

Language: C++ - Size: 338 KB - Last synced at: 2 months ago - Pushed at: over 7 years ago - Stars: 58 - Forks: 9

HOLMS-lib/holms-lib.github.io

HOL Light Library for Modal Systems

Size: 96.7 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

philzook58/Knuckledragger.jl

Julia Semi-Automated Proof Assistant

Language: Julia - Size: 4.88 KB - Last synced at: 4 days ago - Pushed at: 8 months ago - Stars: 3 - Forks: 1

zelosleone/lean-theorems

A repository for studying and implementing Lean theorems, focusing on mathematical and philosophical concepts.

Language: Lean - Size: 12.7 KB - Last synced at: 23 days ago - Pushed at: 23 days ago - Stars: 2 - Forks: 0

neuro-symbolic-ai/explanation_refinement

Code and data for paper "Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving"

Language: Python - Size: 1000 Bytes - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

igreat/tiny-prover

A simple first order logic theorem prover using tableaux

Language: OCaml - Size: 1.13 MB - Last synced at: 3 months ago - Pushed at: 7 months ago - Stars: 1 - Forks: 0