Robert Joseph George

I'm a 4th-year Ph.D. student in Math & CS at Caltech, advised by Anima Anandkumar. I lead our lab's AI4Math effort.

My research is on AI for mathematics, science, and code, and the formal methods needed to verify what these systems produce. I'm gratefully supported by the Caltech Graduate Fellowship, Harmonic AI, Meta, DARPA expMath, NSF AIMing, and the AI for Math Fund from Renaissance Philanthropy, funded by XTX Markets.

Previously, I worked with Amazon's RL team in NYC and graduated from the University of Alberta with the Dean's Silver Medal in Science. I also co-led the ML Theory Reading Group at Cohere for AI, and enjoy teaching and mentoring.

Selected work

All research →

TorchLean

Build, run, and formally verify neural networks in Lean.

Paper Code Project

TorchLean's shared semantics for execution and verification

FloatLib

Floating-point arithmetic, rounding, and numerical proofs in Lean.

Paper Code

FloatLib's numerical representations and certified execution

ITPEvalNeurIPS 2026

Benchmarking formal translation across Lean, Rocq, Isabelle, and HOL Light.

Paper Code

Translation and verification across interactive theorem provers

Latest news

All news →

Oct 2026Our AI4Code research received a grant from Meta to verify AI-generated code, proofs, and specifications.
Oct 2026Gave a talk on Building Trustworthy AI for Mathematics and Science at Cohere Labs.
Oct 2026TorchLean received an AI for Math Fund award from Renaissance Philanthropy, funded by XTX Markets.
Sep 2026Spoke on Verified Scientific Machine Learning in Lean at IPAM, UCLA.
Sep 2026Released FloatLib, our verified floating-point arithmetic library.
Sep 2026Released our stability framework for singularity formation in the 3D Euler equations.