Skip to content
Amitayush Thakur

Amitayush Thakur

Final-year Ph.D. student, UT Austin · advised by Prof. Swarat Chaudhuri

I build AI systems that reason with proofs: LLM agents that write machine-checked proofs, and code generators whose output comes with a formal guarantee that it is correct.

My research sits between AI for mathematics and AI for code: theorem-proving agents in Lean and Coq, benchmarks for formally verified code generation, and systems that discover new mathematics. Before my Ph.D. I spent five years at Microsoft, building distributed services in Azure and doing program synthesis research at Microsoft Research. I studied Computer Science and Mathematics at BITS Pilani.

I’ll graduate in summer 2027 and will be on the job market this year. I’m always open to conversations about research and collaboration in reasoning, AI agents, and verified code generation.

Download CV →Book a meeting →Email me →
Portrait of Amitayush Thakur

§1News

  • New preprint: Harness as a Language, a minimalist agent framework.
  • Started an Applied Science internship at Amazon with the Automated Reasoning Group, working on agent-based proof automation for software verification.
  • ProofWala accepted at ITP 2026.
  • Invited talk at Amazon’s Automated Reasoning Symposium: “End-to-End Verified Code Generation in Lean.”
  • CLEVER and Learning Interestingness (Spotlight) accepted at NeurIPS 2025.

§2Experience

  • 2026Amazon Science
    Applied Science Intern
    Automated Reasoning Group
  • 2025Asari AI
    ML Intern
    Agents for complex systems design
  • 2017–22Microsoft Azure
    Software Engineer II
    Distributed backup services, TLA+
  • 2017Microsoft Research
    Research Intern
    Program synthesis (PROSE)
  • 2016Microsoft Azure
    Summer Intern
    Azure Backup team
  • 2014Bhabha Atomic Research Centre
    Project Trainee
    Network management system

§3Research

All papers →
Thread 1

Theorem-proving agents

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

Thread 2

Verified code generation

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

Thread 3

Neuro-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.

§4Selected papers

Google Scholar →

  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. 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]

  3. Learning Interestingness in Automated Mathematical Theory Formation

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

    NeurIPS 2025★ Spotlight[arXiv][Code]

  4. 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]

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

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

    COLM 2024[Blog][arXiv][Code]

§5Writing

All posts →

§6Also on my mind

I'm increasingly interested in privacy-preserving AI, especially running LLMs under fully homomorphic encryption (FHE). It brings together two things I love: language models, and the number theory and cryptography I grew up reading about.