ericastor / rmzoo
☆14Updated 7 months ago
Related projects ⓘ
Alternatives and complementary repositories for rmzoo
- Tableau for basic modal logic in Lean 3☆13Updated last year
- Book about using Lean with How To Prove It☆15Updated 2 months ago
- mmj2 GUI Proof Assistant for the Metamath project☆72Updated 2 months ago
- Busy Beaver deciders backed by Coq proof☆39Updated 4 months ago
- Mathematical proofs of the bbchallenge project.☆17Updated last week
- Formalizing results about the Mandelbrot set in Lean☆20Updated 2 weeks ago
- ☆10Updated 9 months ago
- A formalization of the Rubik's cube group☆26Updated 4 years ago
- metamath proof enumerators and other things☆87Updated 4 months ago
- Generate HTML documentation for mathlib and Lean☆21Updated last month
- ☆14Updated 11 months ago
- Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.☆27Updated 3 weeks ago
- Matroids in Lean☆18Updated 11 months ago
- Automatically exported from code.google.com/p/ghilbert☆48Updated 7 years ago
- A formal consistency proof of Quine's set theory New Foundations☆66Updated this week
- sorear's Metamath system engine - version 3 Rust☆22Updated last year
- Formalization of the existence of sphere eversions☆36Updated this week
- tool for turning Lean proofs into Blender animations☆41Updated last month
- Formalisations for simplicial HoTT and synthetic ∞-categories.☆45Updated last month
- A formalization of M-types in Agda☆32Updated 4 years ago
- Lean documentation authoring tool☆124Updated this week
- Logic and Mechanized Reasoning☆87Updated 4 months ago
- Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.☆82Updated 3 years ago
- Mathport is a tool for porting Lean3 projects to Lean4☆43Updated this week
- ☆10Updated this week
- Python talking to the Lean theorem prover☆41Updated 3 years ago
- sorear's Metamath system engine☆13Updated 8 years ago
- Methods for accelerating and proving theorems about 5-state Busy Beaver candidates☆19Updated 3 years ago
- Library implementing type inference/checking functionality based on the Lean theorem prover☆39Updated 4 months ago
- Lean theorem prover version 0.2 (it supports standard and HoTT modes)☆121Updated 2 years ago