qedbot

Wikipedia·wikipedia:MeanValueProblem

Mean value problem

conjecture formal record: mixed F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

Fidelity F2: The correspondence is declared through an alignment table and written divergences.

Source

AI activity

How grades work

No AI contribution recorded against this statement.

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through an alignment table and written divergences.

declares divergences from its source

Declared by the projects

1

As each project's formalization.yaml states it.

Smale's mean value conjecture (K = 1): disprooftadamcz/mean-value-problem · joined by anchor · no independent check

Read formalization.yaml

method
autonomous — GPT-6 Astra (pre-release version, OpenAI)
review
other — mechanically verified (comparator: lean kernel replay, standard axioms only) in the harness and again in this repository's ci; no human mathematical review yet (none)
sorry
0 unproved goals declared
sources
Smale's mean value conjecture (K = 1): disproof — other; Smale's mean value conjecture (K = 1) (Wikipedia) — background; The fundamental theorem of algebra and complexity theory — background; Critical points and values of complex polynomials — background
related
google-deepmind/formal-conjectures/blob/9cbe1d3c12998c786b7c2cd99ce28a21b6631f66/FormalConjectures/Wikipedia/MeanValueProblem.lean — builds-on; epoch-research/LeanOpenProblems/blob/0ef96d7b12cfa96a93761b4bba1c635f4546c5ca/apn/data/wikipedia/Isolated/MeanValueProblem.mean_value_problem.lean — builds-on
divergences
The compared theorem is exactly the negation of the Formal Conjectures statement, restated explicitly: for every `p : Polynomial ℂ` with `2 ≤ p.degree`, every `z : ℂ` and every `K : ℝ`, there is `c` with `p.derivative.eval c = 0` and `‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ ‖p.derivative.eval z‖`. The parameter `K` is unused in the Formal Conjectures statement (the constant is fixed at 1). Lean's convention `x / 0 = 0` makes the case `p'(z) = 0` hold trivially with `c = z`, so the formal conjecture is if anything weaker than the informal one; the counterexample uses `z = 0` with `p'(0) = 1`, so it refutes the informal conjecture as stated in the literature.
checked by
nobody independent of its authors yet

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 1
Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 2
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/MeanValueProblem.lean
  • FormalConjectures/Wikipedia/MeanValueProblem.lean

Cite this record

qed.bot, “Mean value problem”, https://qed.bot/s/wikipedia-meanvalueproblem, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.