princeton-vl / CoqGym
A Learning Environment for Theorem Proving with the Coq proof assistant
☆395Updated last year
Alternatives and similar repositories for CoqGym:
Users that are interested in CoqGym are comparing it to the libraries listed below
- Mathematical Components☆604Updated this week
- Lean 3 Theorem Prover (community fork)☆434Updated last year
- The HOL Light theorem prover☆449Updated 2 weeks ago
- Tricks you wish the Coq manual told you [maintainer=@tchajed]☆515Updated last month
- A collection of tools for writing technical documents that mix Coq code and prose.☆250Updated 2 weeks ago
- The agda-unimath library☆242Updated last week
- Metamath Zero specification language☆338Updated 3 months ago
- Metaprogramming, verified meta-theory and implementation of Coq in Coq☆426Updated this week
- A formalization of geometry in Coq based on Tarski's axiom system☆191Updated last month
- ☆162Updated 5 years ago
- 💧 Liquid Tensor Experiment☆189Updated last year
- This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at …☆412Updated this week
- Visual Studio Code extension for Coq☆365Updated this week
- Interactive neural theorem proving in Lean☆118Updated 2 years ago
- CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory☆225Updated last week
- Mathematical Components compliant Analysis Library☆214Updated this week
- ☆40Updated last month
- ☆238Updated last week
- Metamath source file for logic and set theory☆272Updated this week
- Perfectoid spaces in the Lean formal theorem prover.☆118Updated 8 months ago
- Lean 3 material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics. Lean 4 version available here: https://github.com/Imp…☆119Updated last year
- This coq library aims to formalize a substantial body of mathematics using the univalent point of view.☆972Updated this week
- White-box automation for Lean 4☆245Updated last week
- The Lean version manager☆349Updated last month
- Visual Studio Code extension for the Lean 4 proof assistant☆196Updated this week
- Program Synthesis Course☆250Updated 11 months ago
- Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant☆231Updated 3 months ago
- The "batteries included" extended library for the Lean programming language and theorem prover☆288Updated this week
- A Library for Representing Recursive and Impure Programs in Coq☆216Updated last week
- A course on homotopy theory and type theory, taught jointly with Jaka Smrekar☆289Updated last year