Agentic AI
I am exploring how agentic AI can support mathematics at two complementary stages: discovering and checking mathematical arguments, and communicating difficult ideas so that researchers can learn them more quickly and interactively.
Agentic AI for mathematics
Agents for proof discovery and verification
Can an agent help develop a proof while preserving the standards of mathematical argument? I contribute to pipeline-math, a research-stage collaboration spanning learning theory, algebra, number theory, and graph theory.
In the project, GPT-5.5 Pro generates candidate proofs through a prover–verifier workflow. Human contributors then polish and check the resulting write-ups, and selected results are formalized in Lean 4. I contributed to the project’s work on Erdős Problem 477.
Generate and revise candidate proof strategies.
Use agent critique together with human mathematical review.
Translate selected arguments into machine-checked Lean proofs.
Research status: this is a public experimental collection. Only selected results are currently formalized, and the repository explicitly labels partial results.
Explore pipeline-math on GitHubAgentic AI for mathematical communication
From a frontier paper to an interruptible lecture
AI for mathematics can help produce new arguments. A complementary challenge is how those arguments move between people. A difficult paper can demand hours of focused work simply to reconstruct its notation, prerequisites, and proof strategy.
Virtual290 asks what happens when an agent is given a frontier paper and asked to teach it the way we would teach a graduate lecture: working through a theorem on a blackboard, explaining it aloud, and pausing whenever the learner has a question.
Write mathematical arguments on a chalk-style board.
Synchronize narration, notation, annotation, and pointing.
Pause for voice or text questions, revisit a step, and resume.
Research status: synchronized lectures and live questions work in the current prototype; lectures are still authored by hand. An automated paper-to-lecture compiler is the next milestone.
Explore Virtual290 on GitHubOne research agenda
Discover, verify, explain, and question.
Mathematical agents should not only search for answers. They should help us establish confidence in those answers, make difficult reasoning legible to other researchers, and create space for the questions through which understanding develops.
I welcome feedback and collaborators interested in either side of this exploration.