made with anime.js, astro, antigravity
Hi! I'm Simon. I'm a member of technical staff at Mercor in San Francisco, working on synthetic data.
Before that I did research at the UW Math AI Lab, where I was first author on TheoremGraph, and spent two and a half years as a software engineer at Amazon. I graduated from the University of Washington in 2026 with degrees in Mathematics and Informatics. This site has my writing, my work, and blank space for the future.
Work
TheoremGraph, explained in the style of 3Blue1Brown I wrote, animated, and narrated this overview of the paper. 6K+
views on
YouTube
- Extracted the released formal graph of 388K declarations and 11.3M typed edges by running LeanGraph, the lab's Lean 4 elaborator-level extractor, over Mathlib and 24 community projects as Slurm array jobs on UW's HYAK cluster.
- Led the cross-corpus statement matching: embedded 11.7M arXiv statements and all Lean declarations into one semantic space (Qwen3 embeddings, pgvector/HNSW), linking restatements across papers and recovering known informal–formal pairs at 43% top-1 over the full open corpus.
- Beat LeanSearch v2's retriever by +10.3pp Recall@10 on MathlibQR, and showed retrieval raises Claude's autoformalization accuracy from 5/24 to 8/24 unseen Mathlib theorems with 4× fewer tool calls.
- Migrated a Lambda file-processing service to Fargate for a petabyte-scale migration of billions of files (Java 21 virtual threads); stream-buffered multipart I/O raised the per-file limit from a few GB to 2 TiB.
- Replaced 5 manually-scaled CloudSearch domains with serverless OpenSearch via a DynamoDB Streams pipeline, cutting total storage by 66% through document consolidation with upserts.
- Built a workflow observability dashboard for global book publishing with React and Lambda, providing real-time failure diagnostics that eliminated cross-system investigation for 25% of on-call tickets.
- Embedded debugging tools into a legacy JSP dashboard, consolidating cross-region checks into a single interface that eliminated 40+ seconds of navigation per incident.
Publications
- First author of nine (advisors J. Alper, G. Inchiostro, V. Ilin). A unified statement-level dependency graph spanning informal and formal mathematics: 11.7M theorem-like environments parsed from math arXiv with 18.3M candidate dependencies, plus LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declarations and 11.3M typed edges across 25 Lean projects.
- Bridged the two graphs by embedding generated natural-language slogans into a shared semantic space. An LLM judge affirms 47,952 informal–formal matches, with an 87% acceptance rate at cosine similarity ≥ 0.9.
- The same representation improves downstream tasks: retrieval raises correct autoformalizations from 5 to 8 of 24 held-out Mathlib theorems, and reaches 0.883 Recall@10 / 0.739 nDCG@10 on MathlibQR, +10.3pp / +11.6pp over LeanSearch v2's reranked system.
- Released the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and agentic formalization.
Projects
- Applied the TheoremGraph pipeline to 15,458 open problems (UnsolvedMath), surfacing 77 already stated in Lean (RH, Goldbach, PFR, ...) and a "formalization frontier" of unformalized targets.
- Built, with two teammates, a platform for creating controlled environments where LLM agents compete on tasks: a sandbox, an API, and a worker form a closed loop that lets anyone scaffold and evaluate a benchmark in minutes.
- Powered SWECCathon 2026, a hackathon where participants built benchmarks instead of apps (Claude and Gemini playing Jenga, RhetBench, TwisterBench). Now being open-sourced through SWECC Labs.
simonkurgan22 [at] gmail [dot] com