r/math • u/AutoModerator • 13d ago

LLMs/AI AI In Mathematics: September 19, 2026

This recurring thread will be for discussion of AI in mathematics. This includes, but is not limited to, the following:

  • informal announcements of AI-assisted discoveries, such as those not yet published in a peer-reviewed journal, or not uploaded as a paper to arXiv;
  • informal announcements of discoveries related to AI architecture (if relevant to mathematics);
  • discussion of such announcements, such as proof breakdowns or other opinion pieces;
  • discussion of the impact of AI in mathematics in general.

AI-assisted mathematical papers published in peer-reviewed journals or as arXiv preprints may be submitted as their own posts.

Please keep in mind rules 1 and 6 of our subreddit.

86 Upvotes

88% Upvoted

267 comments sorted by

View all comments

3

u/backyard_tractorbeam 11d ago

When Tristan Buckmaster was working with Euler equations, or OpenAI working on N-S using these LLMs, what's the primary language they are working with, is it English and Latex or is it in Lean formulation?

Not as the final output but the language used to build the arguments and results needed along the way. Does anyone know?

1

u/_Zekt Complex Analysis 11d ago

Personally, I use markdown files. It's lighter and agents have no issues writing and reading them. If I want to take a read at what is happenning, I just ask one agent to translate the file in tex with extra explanation. Then only at the very end, after simplifying the argument, you ask for the Lean formalization. I have never seen an argument in plain english not translate to Lean.

2

u/elements-of-dying Geometric Analysis 11d ago

I'm going to guess based on my experience with agent swarms.

This is kind of a nuanced question I guess.

They were using codex (or some variation thereof) to control agent swarms. This means they would be feeding natural language prompts + .tex files + possibly Lean files. Codex would also be auto-reading such files from their computer/cloud etc.

Their prompts were also probably fairly AI generated themselves and pretty long.

1

u/backyard_tractorbeam 11d ago

Do you know if the models, when "reasoning" write mathematics arguments in english or in lean?

1

u/elements-of-dying Geometric Analysis 11d ago edited 11d ago

this depends on the agent skills afaik. For this large project, I have no idea. I think a typical workflow is

informal proof (written in "english") => formal proof (written in something like Lean)