princeton-vl / CoqGymLinks
A Learning Environment for Theorem Proving with the Coq proof assistant
☆415Updated 2 years ago
Alternatives and similar repositories for CoqGym
Users that are interested in CoqGym are comparing it to the libraries listed below
Sorting:
- The HOL Light theorem prover☆496Updated last week
- Program Synthesis Course☆265Updated last year
- IMO Grand Challenge for Artificial Intelligence☆47Updated 3 years ago
- CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory☆236Updated last month
- 💧 Liquid Tensor Experiment☆220Updated last year
- ☆165Updated 6 years ago
- Interactive neural theorem proving in Lean☆132Updated 3 years ago
- Metaprogramming, verified meta-theory and implementation of Rocq in Rocq☆496Updated last week
- Perfectoid spaces in the Lean formal theorem prover.☆129Updated last year
- A collection of tools for writing technical documents that mix Coq code and prose.☆283Updated 4 months ago
- A Learning Environment for Theorem Proving☆76Updated 3 years ago
- ☆44Updated this week
- A formalization of geometry in Coq based on Tarski's axiom system☆201Updated 2 months ago
- Mathematical Components compliant Analysis Library☆232Updated this week
- Multi platform setup for Coq, Coq libraries and tools☆223Updated last week
- Mathematical Components☆664Updated this week
- Visual Studio Code extension for Coq☆428Updated last month
- Tricks you wish the Coq manual told you [maintainer=@tchajed]☆538Updated 7 months ago
- Metamath source file for logic and set theory☆302Updated this week
- Lean 3 material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics. Lean 4 version available here: https://github.com/Imp…☆122Updated last year
- ☆271Updated 10 months ago
- Some Lean tutorials☆183Updated 2 years ago
- A Library for Representing Recursive and Impure Programs in Coq☆239Updated 2 months ago
- Lean Library currently studying for a degree at Imperial College☆229Updated 11 months ago
- Formalization of Machine Learning Theory with Applications to Program Synthesis☆77Updated 2 months ago
- A function definition package for Coq☆236Updated last week
- The agda-unimath library☆282Updated last week
- White-box automation for Lean 4☆335Updated 2 weeks ago
- Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)☆202Updated last week
- Metamath Zero specification language☆369Updated 2 weeks ago