Vasily Ilin

Vasily Ilin

Member of Technical Staff
Axiom Math
Palo Alto, California
vasilin97 (at) gmail.com


About Me

I work at Axiom Math in Palo Alto, California, on large-scale autoformalization of mathematics. I build tools and AI workflows that turn research mathematics into machine-checked proofs in Lean, and make mathematical knowledge easier to find and reuse.

I completed my Ph.D. at the University of Washington, working with Jingwei Hu and Jarod Alper. I am a founding director of the UW Math AI Lab, where my work includes TheoremSearch and TheoremGraph. I also maintain Lean Pool, an AI-maintained archive of formalized mathematics.

I grew up in Russia and moved to Boston in 2015. I studied mathematics as an undergraduate and earned a Master’s in computer science before moving to Seattle for my Ph.D. My earlier research focused on scientific machine learning, score-based methods, and plasma simulation.

Research Interests

News

Publications

  1. Figure from Ternary polynomial relations and periods of cusp forms
    Ternary polynomial relations and periods of cusp forms
    Vasily Ilin, Ken Ono
    arXiv preprint, 2026
    PDF
    A proof of the Bachmann–van Ittersum conjecture and a classification of its polynomial solutions through period polynomials and cusp forms. The main theorems and essential argument are formalized in Lean 4 by AxiomProver.

  2. Figure from Lean Pool: An AI-Maintained Archive of Formalized Mathematics
    Lean Pool: An AI-Maintained Archive of Formalized Mathematics
    Vasily Ilin
    arXiv preprint, 2026
    PDF Code
    An archive of formalized mathematics grown, maintained, and optimized by AI agents, preserving substantial Lean formalizations and making them available for reuse.

  3. Figure from TheoremGraph: Bridging Formal and Informal Mathematics
    TheoremGraph: Bridging Formal and Informal Mathematics
    Simon Kurgan, Evan Wang, Eric Leonen, Sophie Szeto, Luke Alexander, Artemii Remizov, Jarod Alper, Giovanni Inchiostro, Vasily Ilin
    arXiv preprint, 2026
    PDF Code Project Page
    A statement-level dependency graph connecting 11.7 million theorem-like environments from arXiv with 388,105 Lean declarations across 25 projects, bridging formal and informal mathematics for search and retrieval.

  4. Figure from Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium AIPV
    Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
    Vasily Ilin
    AI, Proof and Verification (AIPV), FM 2026 workshop, Tokyo, Japan
    PDF Code
    A complete AI-assisted Lean 4 formalization of the Vlasov–Maxwell–Landau equilibrium characterization, supervised by one mathematician over ten days, with public prompts and development history.

  5. Figure from Semantic Search over 9 Million Mathematical Theorems NeurIPS
    Semantic Search over 9 Million Mathematical Theorems
    Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Jarod Alper, Giovanni Inchiostro, Vasily Ilin
    NeurIPS 2026, Evaluations & Datasets Track (accepted)
    PDF Code Project Page
    A large-scale semantic search system over 9.2 million theorem statements extracted from arXiv and seven other sources, the largest publicly available collection of research-level theorems.

  6. Figure from Learning to Repair Lean Proofs from Compiler Feedback ICLR
    Learning to Repair Lean Proofs from Compiler Feedback
    Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Jarod Alper, Vasily Ilin
    ICLR 2026 Workshop
    PDF Code
    A dataset of 260,000 supervised tuples pairing proof failures with compiler diagnostics, and a fine-tuned 4B-parameter model that surpasses existing approaches in single-shot Lean proof repair.

  7. Figure from A Neural Score-Based Method for Deterministic Collisional Plasma Simulation ICLR
    A Neural Score-Based Method for Deterministic Collisional Plasma Simulation
    Vasily Ilin, Jingwei Hu
    ICLR 2026 Workshop on AI and Partial Differential Equations
    PDF
    A neural network method for deterministic simulation of collisional plasma, inspired by score-based generative modeling.

  8. Figure from DiScoFormer: Plug-In Density and Score Estimation with Transformers ICML
    DiScoFormer: Plug-In Density and Score Estimation with Transformers
    Vasily Ilin, Peter Sushko, Ranjay Krishna
    ICML 2026 Oral
    PDF
    An equivariant Transformer that maps i.i.d. samples to both density values and score vectors, generalizing across distributions and sample sizes, with a principled connection to kernel density estimation.

  9. Figure from Stability of the spatially homogeneous Landau equation in relative entropy and applications to score-based numerical methods
    Stability of the spatially homogeneous Landau equation in relative entropy and applications to score-based numerical methods
    Vasily Ilin
    PDF
    Quantitative stability estimate of the Landau equation in relative entropy, and an application to error analysis of score-based particle methods for simulating plasma.

  10. Figure from Score-Based Deterministic Density Sampling CPAA
    Score-Based Deterministic Density Sampling
    Vasily Ilin, Peter Sushko, Jingwei Hu
    Communications on Pure and Applied Analysis, 2026
    PDF Code Project Page
    Deterministic sampling of an unnormalized density using on-the-fly score estimation.

  11. Figure from RealEdit: Reddit Edits As a Large-scale Empirical Dataset for Image Transformations CVPR
    RealEdit: Reddit Edits As a Large-scale Empirical Dataset for Image Transformations
    Petr Sushko, Ayana Bharadwaj, Zhi Yang Lim, Vasily Ilin, Ben Caffee, Dongping Chen, Mohammadreza Salehi, Cheng-Yu Hsieh, Ranjay Krishna
    CVPR, 2025
    PDF Project Page
    A dataset and a diffusion generative model to perform edits from a prompt. The first global edit model trained on real data.

  12. Figure from Transport based particle methods for the Fokker-Planck-Landau equation CMS
    Transport based particle methods for the Fokker-Planck-Landau equation
    Vasily Ilin, Jingwei Hu, Zhenfu Wang
    Communications in Mathematical Sciences, 2025.
    PDF Code
    An algorithm for simulation of plasma using a neural network, inspired by score-based generative modeling.

  13. Figure from Extending JumpProcesses.jl for fast point process simulation with time-varying intensities JCon
    Extending JumpProcesses.jl for fast point process simulation with time-varying intensities
    Guilherme Augusto Zagatti, Samuel A Isaacson, Christopher Rackauckas, Vasily Ilin, See-Kiong Ng, Stéphane Bressan
    JuliaCon, 2023.
    PDF Code
    An algorithm to efficiently simulate any point process on the real line with a continuous intensity rate.

  14. Figure from Catalyst: Fast and flexible modeling of reaction network PLOS
    Catalyst: Fast and flexible modeling of reaction network
    Torkel E. Loman, Yingbo Ma, Vasily Ilin, Shashi Gowda, Niklas Korsbo, Nikhil Yewale, Chris Rackauckas, Samuel A. Isaacson
    PLOS Computational Biology, 2023
    PDF Code Video
    Julia library for modeling and high-performance simulation of chemical reaction networks.

Selected Talks

  1. JMM
    Deterministic sampling with adaptive score based transport modeling
    Vasily Ilin
    Joint Mathematics Meetings, 2025
    Abstract
    An algorithm for deterministic sampling by integrating the Fokker-Planck equation using particles.

  2. JMM
    Community and Mentorship Through the Experimental Lean Lab
    Jarod Alper, Herman Chau, Vasily Ilin
    Joint Mathematics Meetings, 2025
    Abstract
    Lessons learned in building community and mentoring undergraduate research projects in Lean.

  3. Diffusion Generative Modeling: Making Pictures from Noise with Math
    Vasily Ilin
    UW Math AI seminar
    Abstract Slides
    An SDE-first introduction to diffusion generative modeling.

Work Experience

Academic Service

Reviewing

Teaching Volunteering

Organizing

Open Source Software

Teaching

Instructor

Teaching Assistant

Projects


Powered by Jekyll and Minimal Light theme.