Mike Arpaia
Mathematics
I've been passionate about mathematics for my whole life. My primary interests are in differential geometry, particularly Riemannian geometry, as well as chemical kinetics, fluid dynamics, and formal methods.
I like to work through mathematical ideas by interrogating definitions, testing ideas against examples and visualizations, understanding exactly where a proof needs its assumptions, etc. The process of writing helps me make sense of those connections and explain them to others. I also like to prepare formalizations of concepts in Lean, using notation and proof structure to make formal mathematics readable as exposition.
My background in computer science also shapes how I approach mathematics. Through Conjecture, I'm building tools for writing, formal proof, computation, and working with the literature. I'm also exploring how AI can support mathematical research by exploring different approaches, preserving useful partial results, and leaving reasoning that a mathematician can inspect and build on.
, a Desktop IDE for Mathematics
Coming soon
Conjecture: An open-source desktop app for doing mathematics.
Conjecture is a desktop IDE for mathematics that I'm building. It brings formal proof, learning, mathematical writing, computation, and literature management into a single workspace, with an AI assistant throughout. The desktop app is open source, with an optional cloud platform for AI features, sync, and collaboration.
Conjecture reflects how I work on mathematics: understand an idea, test it on examples, make the argument precise, explain it clearly, and connect it to the literature. I'm building one environment in which these activities can inform one another.
TypeScript67%
Rust31%
Other2%
Coming soon
Conjecture Research: AI research assistant that shows its work.
I'm building an autoresearch system that recursively decomposes mathematical objectives, coordinates parallel agents, and revises its strategies as evidence accumulates. The aim is cumulative mathematical understanding: reusable lemmas, explained failures, and a cited account of what was learned, so a mathematician can inspect the work and develop it further.
Rust97%
Lean3%
Expository Writing
I write expository notes in differential geometry to work through definitions, examples, and proofs in detail. The emphasis is on geometric intuition, the role of assumptions, and making the structure of an argument explicit.
Definitions
Proofs
Expository Formalization
I'm interested in Lean as a medium for mathematical exposition and learning. My aim is to make formal developments readable through motivated definitions, familiar notation, and proofs organized around the mathematical argument. A reader should also be able to inspect assumptions, follow the changing proof state, and work through the next step.
Autoformalization
Autoformalized Lean libraries for reaction kinetics and dynamical systems. These are explicitly autoformalization projects; their notation and proof structure have not received the manual refinement I apply to Lean projects that I work on by hand.