rzach / incompleteness-computabilityLinks
Textbook on Gödel's incompleteness theorems and computability theory
☆20Updated 3 years ago
Alternatives and similar repositories for incompleteness-computability
Users that are interested in incompleteness-computability are comparing it to the libraries listed below
Sorting:
- Open textbook on modal logic☆23Updated 3 years ago
- Tim Button's open textbook on set theory☆37Updated last year
- Textbook on metalogic based on the Open Logic Project☆42Updated last year
- Source of metamath book☆48Updated last year
- A formal proof of an exponentially better upper bound on Ramsey numbers☆17Updated last year
- Coq library for verified low-level programming☆59Updated 7 years ago
- P.D. Magnus' forallx logic textbook☆67Updated 2 months ago
- Busy Beaver deciders backed by Coq proof☆53Updated 3 months ago
- Constructing automata with SAT solvers☆8Updated 6 years ago
- An encyclopedia of proofs☆60Updated 6 months ago
- UCalgary version of forallx, an introduction to formal logic☆107Updated 4 months ago
- Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.☆33Updated last month
- A file-based mirror of the nLab wiki (HTML format).☆24Updated this week
- Metamath program - source code for the Metamath executable☆82Updated 3 weeks ago
- Statements of famous theorems proven in Coq [maintainer=@jmadiot]☆60Updated last year
- An automated theorem prover that uses Büchi automata.☆41Updated 3 years ago
- Continuous functions formalized in Lean4. A students project accompanied by a YouTube video.☆15Updated 10 months ago
- mmj2 GUI Proof Assistant for the Metamath project☆75Updated 8 months ago
- Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintaine…☆75Updated 4 months ago
- ☆30Updated last week
- Binary rational numbers in Coq [maintainer=@herbelin]☆14Updated last year
- A set of files that can be used to create a working version of an early version of the CLU programming language☆36Updated 2 years ago
- Voevodsky's original development of the univalent foundations of mathematics in Coq☆55Updated 10 years ago
- Euclidean plane and its relatives; a minimalist introduction.☆18Updated last month
- Lean proof that a normed vector space with compact unit ball is finite dimensional☆11Updated 5 years ago
- Lecture Notes for Algebra Lectures at the University of Bonn☆12Updated 9 months ago
- Tim Button's Cambridge version of forallx☆13Updated 6 years ago
- A flexible parser generator producing output from object-oriented hierarchical context-free grammar specifications.☆12Updated 3 years ago
- A formal consistency proof of Quine's set theory New Foundations☆71Updated last week
- Write formal proofs in natural language and LaTeX.☆37Updated this week