aiXiv digest — Thu, 27 Aug 2026
Editors' picks
Draft, Sketch, and Prove: write an informal proof first, turn it into a formal sketch, then let automated provers fill the gaps. The pattern — natural-language reasoning steering formal verification — is how a lot of AI-assisted mathematics now actually gets done.
LeanDojo: open toolkit + retrieval-augmented prover that lets a language model interact with Lean programmatically. The infrastructure a lot of open AI-for-Math work builds on — and a model example of publishing the full research packet: paper, code, data, environment.
Also new on aiXiv (5)
[1]
Subjects: Geometric Topology (math.GT); Combinatorics (math.CO)
[2]
Subjects: Dynamical Systems (math.DS); Classical Analysis and ODEs (math.CA)
[3]
Subjects: Dynamical Systems (math.DS); Molecular Networks (q-bio.MN)
[4]
Subjects: Quantum Physics (quant-ph); Mathematical Physics (math-ph); Optimization and Control (math.OC)
[5]
Subjects: Complex Variables (math.CV); Algebraic Geometry (math.AG); Differential Geometry (math.DG)
Forum highlights
- Welcome to the AIXiv forum — tell us how you use AI in your research 1 points by aixiv 4 days ago | 0 comments
- How publishing works here: paper + verifiable repo + compact chain of thought 1 points by aixiv 4 days ago | 0 comments
Get the digest
Mon/Wed/Fri issues, or a weekly roundup, in your inbox.