smale-problems.csvOpen problems sit on the right edge. Hover a point for resolver and notes.
Steve Smale published a list of eighteen problems in 1998. This ledger
scores nineteen rows rather than eighteen problems, because Smale 11 splits
into two subquestions (11a, 11b) that stand separately, and two rows are
recorded as contested rather than resolved or open: general equilibrium
with price adjustments (8) and the limits of intelligence (18).
A "discovery" in this series is a row moving to resolved, dated by the
year of the resolving work. Rows 2, 11b, 14 and 17 are scored from the
secondary consensus account named in their source column. Row 16 is scored
on a different rule, stated in its register entry: an explicit finite
counterexample, independently kernel-checked in Lean and in Isabelle, with
peer review pending; its source column names those verifications rather
than the consensus ledger.
The collection-wide cumulative index redraws the ledger as rows remaining:
"Resolved. Result: Yes, Proved by Grigori Perelman using Ricci flow." — Wikipedia, Smale's problems, problem 2, read 2026-08-14 [@wikipedia2026smale]
"(b) Resolved. Proved by Kozlovski, Shen and van Strien." — Wikipedia, Smale's problems, problem 11, read 2026-08-14 [@wikipedia2026smale]
"Resolved. Result: Yes, solved by Warwick Tucker using a computer-assisted proof combined with normal form techniques." — Wikipedia, Smale's problems, problem 14, read 2026-08-14 [@wikipedia2026smale]
"A counterexample for N ≥ 3 was found by Anthropic employee Levent Alpöge using the LLM Claude Fable 5." — Wikipedia, Smale's problems, problem 16, read 2026-08-14 [@wikipedia2026smale]
The two independent formal verifications the row's source column rests on,
both read 2026-08-14:
"An Independent Lean 4 Verification of the Alpöge–Fable Counterexample" — Zenodo record 21514514, record title, published 2026-07-23 [@zenodo2026jacobian]
"Formal Verification of an Explicit Counterexample to the Jacobian Conjecture" — Archive of Formal Proofs, entry title, dated 2026-07-20 [@afp2026jacobian]
"Finally, P. Lairez found an alternative method to de-randomize the algorithm à la Beltrán-Pardo and thus found a deterministic algorithm which runs in average polynomial time." — Wikipedia, Smale's problems, problem 17, read 2026-08-14 [@wikipedia2026smale]
"There is no consensus whether problem is resolved." — Wikipedia, Smale's problems, problem 18, read 2026-08-14 [@wikipedia2026smale]
The rows are hand-scored: the four pre-2026 resolved rows, the contested
rows and the open rows from the Wikipedia table named in their source
column, and row 16 from the two independent formal verifications named in
the header. There is no fetch.py; a correction means editing the CSV.
figure.py calls the shared problem_list_chart() in
../../lib/families.py with ai_problem="16",
which keeps the rows whose status is resolved with a non-empty
resolved_year and counts resolution events by year from the 1998
list_year to the present. The ai_problem argument is the whole of the AI
coding in the figure: that row's event bar is drawn in the AI colour and
annotated with its short_name and the caption "formal checks complete;
peer review pending"; there is no agent column in the CSV, so the
attribution is a hand-set argument rather than something derived from the
data. The cumulative view is the shared ledger_remaining_chart(), with the
same argument. check.py recomputes the fact lines and the
register entries from the CSV.
One row. Problem 16 (Jacobian conjecture) is a 2026 negative resolution
whose resolver column reads "Levent Alpöge; Claude Fable 5". The Isabelle
verification records the announcement and the stated division of labour:
"This entry gives an independent Isabelle/HOL verification of the explicit three-dimensional map announced by Levent Alpöge on July 20, 2026. The announcement credits Akhil Mathew with prompting the question and the AI system Claude Fable with work leading to the map; stable Lean and independent verification repositories appeared the same day." — Archive of Formal Proofs, Jacobian counterexample entry, abstract, 2026-07-20 [@afp2026jacobian]
The Lean verification states its own standing:
"Status: independent formal verification of a third-party result — not a discovery claim" — Zenodo record 21514514, description, published 2026-07-23 [@zenodo2026jacobian]
No other row's status, resolver or notes carries an AI credit in the
ledger or on the Wikipedia table as of the 2026-08-14 read. Among the
problem-list ledgers in this collection, the
Erdős top-10 subset records one other
AI-attributed resolution (problem 90, 2026).