Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Peano's surface has a strict minimum on every line through the origin but no local extremum

Statement refuted

Refuted: a strict minimum of a function on every line through a point is a local minimum.

Facts & Assumptions

Given: p(x,y)=(y−3x2)(y−x2)p(x,y)=(y-3x^2)(y-x^2).

Counterexample

Proof

technique · direct
1.1

On a nonvertical line y=mxy=mx, p(x,mx)=x2(m−3x)(m−x)p(x,mx)=x^2(m-3x)(m-x), which is positive for sufficiently small nonzero xx when m≠0m\ne0; on y=0y=0 it is 3x4>03x^4>0, and on the vertical line x=0x=0 it is y2>0y^2>0.

givenalgebra
1.2

Along the parabola y=2x2y=2x^2, p(x,2x2)=−x4<0p(x,2x^2)=-x^4<0 for x≠0x\ne0, whereas p(0,0)=0p(0,0)=0.

givenalgebra
2.1

Hence (0,0)(0,0) is a strict linewise minimum but is not a local minimum in the sense of Local and strict local extrema for scalar fields on Euclidean open sets.

step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 8 results over 4 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources