39 results found Sort:

667
4.9k
lgpl-2.1
103
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 developme...
Created 2011-02-17
45,145 commits to master branch, last one 22 hours ago
237
2.8k
apache-2.0
80
A Proof-oriented Programming Language
Created 2014-04-03
38,467 commits to master branch, last one 14 hours ago
216
2.2k
apache-2.0
116
Lean Theorem Prover
This repository has been archived (exclude archived)
Created 2013-07-17
13,725 commits to master branch, last one about a year ago
294
1.7k
apache-2.0
53
Lean 3's obsolete mathematical components library: please use mathlib4
This repository has been archived (exclude archived)
Created 2017-07-21
18,271 commits to master branch, last one about a year ago
LLMs as Copilots for Theorem Proving in Lean
Created 2023-09-09
736 commits to main branch, last one 16 days ago
85
997
other
45
CakeML: A Verified Implementation of ML
Created 2012-10-09
23,821 commits to master branch, last one 12 days ago
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.
Created 2009-10-29
20,439 commits to develop branch, last one a day ago
Tool for data extraction and interacting with Lean programmatically.
Created 2023-06-13
597 commits to main branch, last one 7 days ago
51
392
lgpl-2.1
15
A Learning Environment for Theorem Proving with the Coq proof assistant
Created 2019-05-24
58 commits to master branch, last one about a year ago
106
376
other
36
ACL2 System and Books as Maintained by the Community
Created 2014-09-01
43,643 commits to master branch, last one 11 hours ago
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Created 2021-04-10
285 commits to main branch, last one 2 days ago
Retrieval-Augmented Theorem Provers for Lean
Created 2023-03-16
125 commits to main branch, last one 20 days ago
Proving Ground: Tools for Automated Mathematics
Created 2013-02-20
4,300 commits to master branch, last one 3 years ago
llmstep: [L]LM proofstep suggestions in Lean 4.
Created 2023-07-08
73 commits to master branch, last one about a year ago
12
116
bsd-3-clause
8
Tableau-based Theorem Prover for Natural Logic and Language
Created 2017-03-05
138 commits to master branch, last one 2 years ago
ChatGPT plugin for theorem proving in Lean
Created 2023-06-21
14 commits to main branch, last one 10 months ago
9
109
apache-2.0
3
A project to digitalise results from physics into Lean. (formally called HepLean)
Created 2024-04-16
1,559 commits to master branch, last one a day ago
18
97
gpl-3.0
13
GAPT: General Architecture for Proof Theory
Created 2011-06-29
7,646 commits to master branch, last one 4 months ago
8
96
apache-2.0
5
Jupyter kernel for Coq
Created 2018-12-26
155 commits to master branch, last one about a year ago
10
92
apache-2.0
6
Resolution theorem proving for predicate logic in pure Python.
Created 2017-03-04
96 commits to master branch, last one about a year ago
17
84
bsd-2-clause
11
Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
Created 2016-02-06
659 commits to master branch, last one 4 months ago
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Created 2024-05-27
14 commits to master branch, last one 8 months ago
コード例で学ぶ Lean 言語
Created 2023-09-15
2,063 commits to main branch, last one a day ago
Public code developed during my MSc study at University of Bologna
Created 2015-10-28
130 commits to master branch, last one 2 years ago
4
76
other
9
Book: Introduction to Dependent Types with Idris
Created 2018-08-01
328 commits to master branch, last one about a year ago
A Low Barrier Proof Assistant
Created 2022-11-08
178 commits to main branch, last one 3 days ago
15
73
apache-2.0
9
A Learning Environment for Theorem Proving
Created 2018-05-31
599 commits to master branch, last one 5 years ago
Athena is a modern, practical language for proof engineering & natural deduction.
Created 2022-05-02
135 commits to master branch, last one 2 months ago
An environment for learning formal mathematical reasoning from scratch
Created 2022-02-10
263 commits to main branch, last one 6 months ago