---
id: "2026-10-09-smale-sixth-problem-five-bodies-lean-tomar"
url: "https://postcutoff.com/e/2026-10-09-smale-sixth-problem-five-bodies-lean-tomar/"
as_of: "2026-10-12T22:30:00+02:00"
date: "2026-10-09"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Peer-reviewed
sources: 3
editor: Adam Bicz
human_review: null
version: null
---

As of: 2026-10-12 22:30 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/e/2026-10-09-smale-sixth-problem-five-bodies-lean-tomar/

# Smale's sixth problem claimed for five bodies in the plane

Full title: Smale's sixth problem claimed for five bodies in the plane: finitely many central configurations for all positive masses, AI-found and proved in Lean (Tomar)

On 9 Oct 2026 Tejasvi Singh Tomar (independent researcher) posted arXiv 2610.13100: for every choice of five positive masses the planar five-body problem has finitely many central configurations up to similarity. This is Smale's sixth problem for n = 5 in the plane; Albouy and Kaloshin (Annals of Mathematics, 2012) had proved it outside a codimension-two set of masses. The paper says the theorem "is proved in Lean 4 with Mathlib" and is accepted by two independent kernel implementations, and its "Use of AI tools" note reads: "Generative AI tools were used to find and prove the results, to write the programs and the Lean formalization, and to draft the text." Unrefereed; no expert reaction found yet.

## Key facts
- Paper: 'Finiteness of planar central configurations of five bodies for all positive masses', arXiv 2610.13100 [math.DS], 9 Oct 2026; Tejasvi Singh Tomar, 'Independent researcher'; 91 pages
- Theorem 1.1: 'For every m ∈ (R>0)^5 the planar five-body problem with masses m has finitely many central configurations up to similarity.'
- Smale's sixth problem (1998) asks whether the number of central configurations is finite for every choice of positive masses. Known before: n = 3 (five configurations, Euler and Lagrange), n = 4 (Hampton–Moeckel 2006), n = 5 for masses outside a closed algebraic subset of codimension two (Albouy–Kaloshin 2012)
- Method: follows Albouy and Kaloshin's singular-sequence diagrams; determines the possible valuation vectors at all positive masses, excludes diagrams by expanding the potential at a place, then an exact computer-algebra analysis with 'exact rational certificates'
- Special masses: on the rays through (1,4,4,4,4) and (1,1,4,4,4) the complex equations can have a continuum of solutions, so the real configurations are counted directly: 306 and 294 up to orientation-preserving similarity
- Formal proof: 'Theorem 1.1 is proved in Lean 4 with Mathlib … It is also accepted by nanoda and lean4lean, two independent implementations of the Lean kernel.' The paper says re-running the computations from a fresh copy takes about 860 CPU-hours
- AI disclosure ('Use of AI tools'): 'Generative AI tools were used to find and prove the results, to write the programs and the Lean formalization, and to draft the text.' No model is named
- Certificates, checking programs and the Lean project are archived at doi.org/10.5281/zenodo.23202861
- The same author posted a second AI-generated, Lean-checked result the day before: the rank of 3×3 matrix multiplication over F_2 is 23 (arXiv 2610.11823)
- Scope: the plane and five bodies only; Smale's problem for n ≥ 6 stays open

## What happened

A central configuration is an arrangement of point masses in which the gravitational pull on each body points to the common centre
of mass and is proportional to the distance from it. Such arrangements are the shapes that can rotate rigidly or collapse
homothetically. Whether there are only finitely many of them for given masses is the sixth problem on Steve Smale's 1998 list of
problems for the 21st century. Four bodies were settled in 2006. For five bodies in the plane, Alain Albouy and Vadim Kaloshin
proved finiteness in 2012 except for masses in an explicit exceptional set.

Tomar's paper claims to remove that exceptional set. It keeps the Albouy–Kaloshin framework, adds expansions of the potential that
rule out more limiting diagrams, and settles what remains by exact computer algebra with rational certificates. For two special
families of masses, where the complexified equations genuinely have infinitely many solutions, it counts the real configurations
directly.

The author states that generative AI tools found and proved the results and wrote the Lean formalization. The Lean proof of the
main theorem is reported to pass the standard kernel and two independent re-implementations.

## Why it matters

If it holds, it closes a case of a famous problem with a machine-checked proof produced largely by AI, by someone outside a
university. A Lean proof shifts the question from "is the argument right" to "does the formal statement say what the theorem
says". The paper points to the file with the formal statement so readers can compare, but nobody else is known to have done that
yet.

## What is disputed or not yet verified

- Verification: Lean 4 proof reported, accepted by the Lean kernel and by nanoda and lean4lean; unrefereed preprint, the formal statement has not been audited by others

The Lean project was not rebuilt for this entry. The paper does not say which models were used. No reaction from specialists in
celestial mechanics was found on 12 Oct 2026.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 162 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 101 days after its cutoff
- Gemini 3.8 Flash (training cutoff March 2026): 192 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 131 days after its cutoff

## Sources

1. [arXiv 2610.13100: Finiteness of planar central configurations of five bodies for all positive masses](https://arxiv.org/abs/2610.13100) (arxiv.org, paper)
2. [Zenodo archive: certificates, checkers and Lean project](https://doi.org/10.5281/zenodo.23202861) (doi.org, code)
3. [Albouy & Kaloshin, Finiteness of central configurations of five bodies in the plane (Annals of Mathematics, 2012)](https://doi.org/10.4007/annals.2012.176.1.10) (doi.org, paper)

## Changes

- 2026-10-12 (filed): Created from the arXiv PDF (found by a manual arXiv scan)

## Related

- 2026-10-09: [Thurston's geometrization conjecture formalised in Lean](https://postcutoff.com/e/2026-10-09-geometrization-conjecture-lean-formalization/index.md)
- 2026-10-08: [Laderman's 23 multiplications are optimal for 3×3 matrices over F_2 and over the integers](https://postcutoff.com/e/2026-10-08-rank-3x3-matrix-multiplication-f2-is-23-lean-tomar/index.md)
- 2026-09-30: [Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help](https://postcutoff.com/e/2026-09-30-ai-assisted-conjecture-wave-summer-2026/index.md)