Amitayush Thakur amit9oct

• University of Texas at Austin

• United States of America

Pinned Loading

1. COPRA: An in-COntext PRoof Agent which uses LLMs like GPTs to prove theorems in formal languages.

   Python 70 12

2. An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.

   Lean 222 33

3. CLEVER: Code Lean Evaluation for Verified End-to-end Reasoning

   Lean 38 6

4. Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving.

   Python 19 1

5. Library for interaction with proof-environments, proof search and training of transformers for proof-step prediction

   Python 9

6. Toy-Compiler can be for educational purpose. Helpful for those who need to design a compiler for a simple language. It has the complete compiler built in C language which includes lexer,parser and …

   C 1