Skip to content
Amitayush Thakur
Research

Papers & talks

How can machines reason rigorously? I approach that question through formal proof: if an AI's output can be checked by a proof assistant, we never have to take it on trust.

§1Theorem-proving agents

LLM agents, benchmarks, and data pipelines for writing machine-checked proofs in Lean, Coq, and Isabelle.

  1. ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving

    Amitayush Thakur, George Tsoukalas, Greg Durrett, Swarat Chaudhuri

    ITP 2026[Paper][arXiv][Code]

  2. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition

    George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, Swarat Chaudhuri

    NeurIPS 2024★ Best Paper, AI for Math Workshop @ ICML 2024[Website][arXiv][Code]

  3. An In-Context Learning Agent for Formal Theorem-Proving

    Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, Swarat Chaudhuri

    COLM 2024[Blog][arXiv][Code]

§2Verified code generation

Generating programs together with formal specifications and proofs that they are correct.

  1. CLEVER: A Curated Benchmark for Formally Verified Code Generation

    Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche, Greg Durrett, Yisong Yue, Swarat Chaudhuri

    NeurIPS 2025[arXiv][Code]

§3Neuro-symbolic AI

Pairing LLMs with symbolic structure: programming languages that agents think and act in, and systems that discover mathematics by inventing concepts and judging which ones are interesting.

  1. Harness as a Language: A Minimalist Agent Framework With Maximal Expressivity

    Z. Li, J. Liu, M. Vukelic, N. Shen, S. Lall, Amitayush Thakur, A. Zhang, O. Khattab, J. Light, A. Solar-Lezama

    Preprint[arXiv]

  2. Learning Interestingness in Automated Mathematical Theory Formation

    George Tsoukalas, Rahul Saha, Amitayush Thakur, Sabrina Reguyal, Swarat Chaudhuri

    NeurIPS 2025★ Spotlight[arXiv][Code]

§4Earlier work

  1. A Distributed Algorithm for Balanced Multi-Robot Task Allocation

    A. Gautam, Amitayush Thakur, G. Dhanania, S. Mohan

    ICIIS 2016[IEEE]

§5Invited talks

  • “End-to-End Verified Code Generation in Lean” · Amazon Automated Reasoning Symposium
  • “CLEVER: A Benchmark for Two-staged, End-to-end Verified Code Generation” · TPC25, Trillion Parameter Consortium
  • “Advancing Theorem Proving with AI: The Power of Large Language Models” · Rutgers, Department of Mathematics