Misc

I am interested in formalizing foundational results in complex algebraic geometry. Example projects include the Analytic Weierstrass Preparation Theorem and the Analytic Nullstellensatz. More to come.

I make sure these formalizations pass Comparator testing and are sound. They are also available through the Palomar Registry.

I have also formalized my paper To cover a permutohedron (with Ji Zeng) in Lean. This project relies on the Weierstrass Preparation Theorem (WPT) formalization above. Both developments ultimately rest on Mathlib and its dependencies, with no additional axioms.

I am enthusiastic about using AI-assisted methods to pursue results that I find elegant and worth developing. Most of these projects will concern geometry. I will experiment with different workflows for different types of investigation, sometimes incorporating input from experts.

I verify each result myself whenever it lies within my expertise. Otherwise, I consult experts. If related work is made public, I will disclose the role of AI. For results in algebraic geometry and closely related areas, readers may assume that I understand the main proof.

• Can arXiv Keep Up with the AI Era? September 9, 2026

  The recent discussion about AI math papers and arXiv makes me think of GitHub. Both platforms seem to be struggling to keep up with the AI era.

  GitHub projects receive annoying pull requests from AI bots or people submitting AI-generated code. The concern about arXiv being flooded with AI-generated papers is similar: submissions are cheap to produce, but expensive for others to review.

  GitHub also has a separate problem: its own infrastructure contains too much vibe-coded AI slop. That issue is not yet as visible with arXiv.

  Still, GitHub offers something useful: GitHub Actions lets projects build flexible, automated workflows around submissions. It is harder to see how arXiv could adopt that model, but Palomar looks like an early attempt to move mathematical infrastructure in this direction.

  What the right infrastructure for mathematical discovery should look like in this era remains an open question.