lean-dojo/LeanDojo

Tool for data extraction and interacting with Lean programmatically.

Language: Python - Size: 2.11 MB - Last synced: 1 day ago - Pushed: 1 day ago - Stars: 453 - Forks: 66

arylwen/mlk8s

microk8s based ml cluster

Language: Jupyter Notebook - Size: 65.3 MB - Last synced: 1 day ago - Pushed: 1 day ago - Stars: 1 - Forks: 0

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: 110 MB - Last synced: 1 day ago - Pushed: 2 days ago - Stars: 595 - Forks: 129

sean-lamont/bait

Language: Standard ML - Size: 71.5 MB - Last synced: 2 days ago - Pushed: 3 days ago - Stars: 4 - Forks: 1

cheuktingli/psitip

Python Symbolic Information Theoretic Inequality Prover

Language: Python - Size: 2.56 MB - Last synced: 2 days ago - Pushed: 3 months ago - Stars: 32 - Forks: 7

philzook58/knuckledragger

Language: Jupyter Notebook - Size: 314 KB - Last synced: 4 days ago - Pushed: 4 days ago - Stars: 4 - Forks: 1

lean-dojo/LeanCopilot

LLMs as Copilots for Theorem Proving in Lean

Language: C++ - Size: 1.1 MB - Last synced: 4 days ago - Pushed: 4 days ago - Stars: 808 - Forks: 70

gapt/gapt

GAPT: General Architecture for Proof Theory

Language: Scala - Size: 181 MB - Last synced: 2 days ago - Pushed: 2 days ago - Stars: 91 - Forks: 18

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: 278 KB - Last synced: 4 days ago - Pushed: 7 days ago - Stars: 265 - Forks: 8

leanprover/lean3 📦

Lean Theorem Prover

Language: C++ - Size: 50.3 MB - Last synced: 4 days ago - Pushed: 7 months ago - Stars: 2,138 - Forks: 216

Inferara/inferara.com

An official website

Language: HTML - Size: 289 KB - Last synced: 10 days ago - Pushed: 10 days ago - Stars: 0 - Forks: 0

mrtkp9993/MathProg

Automated theorem proving, Logic Programming, Optimization examples.

Language: Python - Size: 24.4 KB - Last synced: 11 days ago - Pushed: about 2 years ago - Stars: 1 - Forks: 0

tilk/LambdaCert Fork of progval/LambdaCert

Certified LambdaJS semantics and interpreter.

Language: Coq - Size: 4.5 MB - Last synced: 11 days ago - Pushed: over 7 years ago - Stars: 3 - Forks: 0

tani/solv

IPC/CPC theorem prover in Prolog

Language: Prolog - Size: 48.8 KB - Last synced: 11 days ago - Pushed: 2 months ago - Stars: 1 - Forks: 0

Gbury/dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

Language: OCaml - Size: 10.1 MB - Last synced: 12 days ago - Pushed: 12 days ago - Stars: 75 - Forks: 16

coq-tactician/coq-tactician-api

An API for interfacing with Coq through Tactician by external agents

Language: Python - Size: 1.19 MB - Last synced: 12 days ago - Pushed: 13 days ago - Stars: 1 - Forks: 0

thery/mathcomp-extra

Extra contribution for mathcomp

Language: Coq - Size: 742 KB - Last synced: 10 days ago - Pushed: 3 months ago - Stars: 5 - Forks: 2

vvulpes0/Language-Toolkit-2

A set of tools for analyzing languages via logic and automata

Language: Haskell - Size: 1.88 MB - Last synced: 13 days ago - Pushed: 15 days ago - Stars: 21 - Forks: 0

sushmaakoju/research-experience

Research experience

Size: 32 MB - Last synced: 16 days ago - Pushed: 25 days ago - Stars: 0 - Forks: 0

leanprover-community/mathlib

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

Language: Lean - Size: 213 MB - Last synced: 18 days ago - Pushed: 22 days ago - Stars: 1,632 - Forks: 294

evhub/pyprover

Resolution theorem proving for predicate logic in pure Python.

Language: Python - Size: 344 KB - Last synced: 11 days ago - Pushed: 6 months ago - Stars: 88 - 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: 18 days ago - Pushed: 19 days ago - Stars: 14 - Forks: 1

jonaprieto/agda-metis

Metis Prover Reasoning for Propositional Logic in Agda

Language: Agda - Size: 765 KB - Last synced: 19 days ago - Pushed: over 5 years ago - Stars: 1 - Forks: 1

veracruz-project/supervisionary

The Supervisionary proof-checking kernel for higher-order logic

Language: Rust - Size: 827 KB - Last synced: 19 days ago - Pushed: about 2 years ago - Stars: 3 - Forks: 0

brendanny/natural-number-game

Learning how to use the Lean theorem prover

Size: 4.88 KB - Last synced: 18 days ago - Pushed: 19 days ago - Stars: 0 - Forks: 0

lean-dojo/LeanDojoWebsite

Code for LeanDojo's website

Language: JavaScript - Size: 31 MB - Last synced: 19 days ago - Pushed: 20 days ago - Stars: 7 - Forks: 1

wellecks/llmstep

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

Language: Python - Size: 1.56 MB - Last synced: 15 days ago - Pushed: 6 months ago - Stars: 92 - Forks: 13

c-cube/quip-book

Book for Quip, a proof format for first-order and higher-order theorem provers

Language: SMT - Size: 1.21 MB - Last synced: 23 days ago - Pushed: about 1 year ago - Stars: 3 - Forks: 0

shilangyu/unambiguous-grammar

Formal specification of a language of grammars and proofs about their ambiguity

Language: Coq - Size: 14.6 KB - Last synced: 26 days ago - Pushed: 26 days ago - Stars: 0 - Forks: 0

acl2/acl2

ACL2 System and Books as Maintained by the Community

Language: Common Lisp - Size: 1.2 GB - Last synced: 28 days ago - Pushed: 28 days ago - Stars: 336 - Forks: 96

coq/coq

Coq is a formal proof management system. 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: 185 MB - Last synced: 29 days ago - Pushed: 29 days ago - Stars: 4,596 - Forks: 627

CakeML/cakeml

CakeML: A Verified Implementation of ML

Language: Standard ML - Size: 102 MB - Last synced: 29 days ago - Pushed: 29 days ago - Stars: 911 - Forks: 81

FStarLang/FStar

A Proof-oriented Programming Language

Language: F* - Size: 725 MB - Last synced: 29 days ago - Pushed: 29 days ago - Stars: 2,558 - Forks: 231

lean-dojo/ReProver

Retrieval-Augmented Theorem Provers for Lean

Language: Python - Size: 1.65 MB - Last synced: 30 days ago - Pushed: about 1 month ago - Stars: 158 - Forks: 27

lagenorhynque/semantics-of-programming-languages

Study notes on semantics of programming languages & theorem proving

Language: Idris - Size: 14.6 KB - Last synced: 29 days ago - Pushed: almost 7 years ago - Stars: 1 - Forks: 0

rhaver/pvs-protocol-verification

Verifying Multi-party Authentication Using Rank Functions and PVS

Size: 652 KB - Last synced: about 1 month ago - Pushed: about 2 years ago - Stars: 0 - Forks: 0

yazaldefilimone/lean.prover

Lean is a dependently-typed programming language and theorem prover.

Language: Lean - Size: 1000 Bytes - Last synced: 30 days ago - Pushed: about 1 month ago - Stars: 0 - Forks: 0

mwb-cde/hseq-prover

Theorem prover for higher order logic

Language: OCaml - Size: 15.4 MB - Last synced: about 1 month ago - Pushed: over 2 years ago - Stars: 0 - Forks: 0

johnyf/tool_lists

Links to tools by subject

Size: 63.5 KB - Last synced: 24 days ago - Pushed: about 2 months ago - Stars: 360 - Forks: 81

dtumad/lean-crypto-formalization

Library for formalizing cryptography proofs in Lean 3 (Deprecated)

Language: Lean - Size: 2.13 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 7 - Forks: 0

somombo/supertype

Lean Subtypes that have Super powers

Language: Lean - Size: 12.7 KB - Last synced: 11 days ago - Pushed: 6 months ago - Stars: 1 - Forks: 0

tlaplus-workshops/ewd998

Distributed termination detection on a ring, due to Shmuel Safra:

Language: TLA - Size: 1.95 MB - Last synced: 18 days ago - Pushed: 7 months ago - Stars: 46 - Forks: 47

uuverifiers/ostrich

An SMT Solver for string constraints

Language: Scala - Size: 207 MB - Last synced: 19 days ago - Pushed: 19 days ago - Stars: 29 - Forks: 8

LS-Lab/orbital

Orbital Library

Language: Java - Size: 4.7 MB - Last synced: about 2 months ago - Pushed: about 7 years ago - Stars: 7 - Forks: 3

idris-hackers/software-foundations

Software Foundations in Idris

Language: Idris - Size: 4.25 MB - Last synced: 29 days ago - Pushed: almost 5 years ago - Stars: 446 - Forks: 34

thery/coqprime

Prime numbers for Coq

Language: Coq - Size: 13 MB - Last synced: 10 days ago - Pushed: about 2 months ago - Stars: 37 - Forks: 18

triska/presprover

Prove formulas of Presburger Arithmetic

Language: Prolog - Size: 34.2 KB - Last synced: about 2 months ago - Pushed: about 4 years ago - Stars: 7 - Forks: 2

hengxin/tlaps-examples

Examples for TLAPS (TLA+ Proof System)

Language: TeX - Size: 4.76 MB - Last synced: 27 days ago - Pushed: about 4 years ago - Stars: 9 - Forks: 6

theoremprover-museum/egal

Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory

Language: OCaml - Size: 1.32 MB - Last synced: about 1 month ago - Pushed: almost 3 years ago - Stars: 2 - Forks: 0

FilippoFantinato/type-theory

Type Theory course ; Master's Degree in Computer Science @ UniPD

Language: Agda - Size: 53.7 KB - Last synced: 2 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

dselsam/certigrad

Bug-free machine learning on stochastic computation graphs

Language: Lean - Size: 289 KB - Last synced: about 2 months ago - Pushed: about 5 years ago - Stars: 385 - Forks: 34

princeton-vl/CoqGym

A Learning Environment for Theorem Proving with the Coq proof assistant

Language: Coq - Size: 32 MB - Last synced: 2 months ago - Pushed: 11 months ago - Stars: 365 - Forks: 50

Coq-Polyhedra/Coq-Polyhedra

Formalizing convex polyhedra in Coq

Language: Coq - Size: 116 MB - Last synced: about 2 months ago - Pushed: about 2 months ago - Stars: 20 - Forks: 4

thery/minirubik

Solving the mini Rubik (2x2) in Coq

Language: Coq - Size: 164 KB - Last synced: 19 days ago - Pushed: 11 months ago - Stars: 4 - Forks: 0

siddhartha-gadgil/ProvingGround

Proving Ground: Tools for Automated Mathematics

Language: Jupyter Notebook - Size: 435 MB - Last synced: 20 days ago - Pushed: over 2 years ago - Stars: 202 - Forks: 38

fsestini/zsyntax

Automated theorem prover for a linear logic-based calculus for molecular biology.

Language: Haskell - Size: 709 KB - Last synced: 29 days ago - Pushed: 11 months ago - Stars: 11 - Forks: 0

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

DominicPM/supervisionary

Supervisionary: a proof-checking system for HOL

Language: Rust - Size: 4.84 MB - Last synced: 3 months ago - Pushed: about 1 year ago - Stars: 0 - Forks: 0

thery/EdwardsEllipticCurve

Group Law for Elliptic Curves according to Tom Hales

Language: Coq - Size: 275 KB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 1 - Forks: 0

hanwenzhu/primality-tests

Miller–Rabin primality test in Lean

Language: Lean - Size: 63.5 KB - Last synced: about 2 months ago - Pushed: 4 months ago - Stars: 2 - Forks: 0

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

input-output-hk/equivalence-reasoner

An automated equivalence reasoner for Isabelle/HOL

Language: Isabelle - Size: 57.6 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 2 - Forks: 4

EugeneLoy/coq_jupyter

Jupyter kernel for Coq

Language: Python - Size: 411 KB - Last synced: 19 days ago - Pushed: 4 months ago - Stars: 89 - Forks: 7

gpoesia/peano

An environment for learning formal mathematical reasoning from scratch

Language: Python - Size: 674 KB - Last synced: 3 months ago - Pushed: about 1 year ago - Stars: 27 - Forks: 1

jonaprieto/agda-prop

A Library for Classical Propositional Logic in Agda

Language: Agda - Size: 442 KB - Last synced: 19 days ago - Pushed: over 4 years ago - Stars: 15 - Forks: 1

Lix0120/eudoxus

Formalise Eudoxus reals in lean and prove they form a complete Archimedean ordered field.

Language: Lean - Size: 123 KB - Last synced: 4 months ago - Pushed: about 3 years ago - Stars: 6 - Forks: 1

UofSC-Spring-2023-SCHC-411-H01/homework02

Writing some propositions and giving some proofs in Lean

Language: Lean - Size: 5.86 KB - Last synced: 4 months ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0

coq-tactician/coq-tactician

A Seamless, Interactive Tactic Learner and Prover for Coq

Language: OCaml - Size: 2.17 MB - Last synced: 19 days ago - Pushed: 19 days ago - Stars: 51 - Forks: 16

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

Forked sources for HOL4 theorem-proving system (for sending PRs)

Language: Standard ML - Size: 116 MB - Last synced: 29 days ago - Pushed: 29 days ago - Stars: 6 - Forks: 2

workflowfm/workflowfm-reasoner

A logic-based library for correct-by-construction process modelling and composition.

Language: OCaml - Size: 4.19 MB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 1 - 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: 3 months ago - Pushed: 4 months ago - Stars: 1 - Forks: 0

dominique-unruh/scala-isabelle

A Scala library for controlling/interacting with Isabelle

Language: Scala - Size: 1.21 MB - Last synced: 8 months ago - Pushed: 8 months ago - Stars: 32 - Forks: 8

choukh/Set-Theory

A formalization of the textbook Elements of Set Theory

Language: Coq - Size: 3.79 MB - Last synced: 3 months ago - Pushed: over 2 years ago - Stars: 57 - Forks: 5

potassco/anthem

🎼 Translate answer set programs to first-order theorem prover language

Language: Rust - Size: 1.37 MB - Last synced: 3 months ago - Pushed: over 3 years ago - Stars: 7 - Forks: 5

aztek/atp

Haskell interface to automated theorem provers

Language: Haskell - Size: 352 KB - Last synced: 21 days ago - Pushed: over 2 years ago - Stars: 6 - Forks: 0

ice1k/Theorems

:globe_with_meridians: Theorems that rule this multiverse

Language: Agda - Size: 76.2 KB - Last synced: 11 days ago - Pushed: over 5 years ago - Stars: 11 - Forks: 2

leoprover/Leo-III

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

Language: Scala - Size: 30.3 MB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 35 - Forks: 6

uncomputable/expressive-wallet

What is a minimal wallet of coins that can express all amounts below a target?

Language: Coq - Size: 30.3 KB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 0 - Forks: 0

kaicho8636/proposition_theory_python

Definitions and proofs written in Python

Language: Python - Size: 46.9 KB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 0 - Forks: 0

OolonColoophid/bakerStreet

A natural deduction helper for macOS

Language: Swift - Size: 46.7 MB - Last synced: 6 months ago - Pushed: over 3 years ago - Stars: 2 - Forks: 0

kovvalsky/prove_SICK_NL

Prove Ducth NLI problems of SICK-NL with LangPro

Language: Prolog - Size: 66.4 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 3 - Forks: 0

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: 5 months ago - Pushed: 5 months ago - Stars: 12 - Forks: 1

katrinafyi/madeline

madeline/Proof General: an integrated prover environment for our favourite deductive logic games.

Language: C++ - Size: 9.43 MB - Last synced: 19 days ago - Pushed: 8 months ago - Stars: 4 - Forks: 0

muraliadithya/mini-sygus

a constraint-based syntax-guided synthesis (SyGuS) engine

Language: Python - Size: 267 KB - Last synced: 20 days ago - Pushed: over 1 year ago - Stars: 9 - Forks: 0

gebner/trepplein

Lean type-checker written in Scala.

Language: Scala - Size: 118 KB - Last synced: 7 months ago - Pushed: about 2 years ago - Stars: 26 - Forks: 3

pro465/nnoq

not noq

Language: Rust - Size: 94.7 KB - Last synced: 3 months ago - Pushed: 7 months ago - Stars: 4 - Forks: 1

VTrelat/Hopcroft_verif

Formal verification in Isabelle(HOL) of Hopcroft's algorithm for minimizing DFAs including runtime analysis

Language: Isabelle - Size: 16.2 MB - Last synced: 8 months ago - Pushed: 8 months ago - Stars: 1 - Forks: 0

acuarica/hsc 📦

The Haskell Supercompiler Project aims to bring back supercompilation to Haskell.

Language: Haskell - Size: 38.5 MB - Last synced: 15 days ago - Pushed: about 1 year ago - Stars: 1 - Forks: 0

fadoss/maude2lean

Maude to Lean translator

Language: Lean - Size: 175 KB - Last synced: 8 months ago - Pushed: 8 months ago - Stars: 0 - Forks: 0

jonaprieto/athena 📦

Translates Metis ATP proofs to the Agda code

Language: TeX - Size: 15.1 MB - Last synced: 19 days ago - Pushed: about 4 years ago - Stars: 6 - Forks: 2

bor0/gidti

Book: Introduction to Dependent Types with Idris

Size: 10.9 MB - Last synced: 2 months ago - Pushed: about 1 year ago - Stars: 73 - Forks: 4

enshankar/BigProof

Collaborative repo for Big Proof Programme at the Isaac Newton Institute, Jun 26 to Aug 4, 2017

Size: 20.5 KB - Last synced: 8 months ago - Pushed: almost 7 years ago - Stars: 0 - Forks: 0

hwixley/AR-Coursework1

Theorem proving in Isabelle

Language: Isabelle - Size: 587 KB - Last synced: 9 months ago - Pushed: about 3 years ago - Stars: 0 - Forks: 0

leoprover/ddl2thf 📦

DDL2THF -- A preprocessor for translating problems in Dyadic Deontic Logic into THF problems

Language: Java - Size: 325 KB - Last synced: 9 months ago - Pushed: about 2 years ago - Stars: 0 - Forks: 0

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: 6 months ago - Pushed: 10 months ago - Stars: 24 - Forks: 3

rechim25/theorem-prover

Satisfiability tester for propositional logic.

Language: C - Size: 24.4 KB - Last synced: 9 months ago - Pushed: about 3 years ago - Stars: 0 - Forks: 0

chrisjpm/holbert Fork of liamoc/holbert

A graphical interactive proof assistant designed for education. My contributions: applying rules by elimination, proofs by induction, proofs by cases, multi-axiom element and misc css styling. Honours report grade: 76% :tada:

Language: Haskell - Size: 13.3 MB - Last synced: 9 months ago - Pushed: almost 2 years ago - Stars: 0 - Forks: 0

Kamirus/lambda-formalizations

Lambda Calculi Formalizations in Coq using nested datatypes for a type-safe term representation

Language: Coq - Size: 388 KB - Last synced: 19 days ago - Pushed: over 1 year ago - Stars: 4 - Forks: 1

Edward-Ji/LogicSolver

A propositional logic equivalence and first-order logic ND prover (wrapper).

Language: Python - Size: 57.6 KB - Last synced: 21 days ago - Pushed: about 1 year ago - Stars: 0 - Forks: 0

MarisaKirisame/first_order_logic_prover

Language: C++ - Size: 338 KB - Last synced: 9 months ago - Pushed: about 6 years ago - Stars: 57 - Forks: 9