qinz1yang claims the released Lean 4 differential-geometry library formalizes the Hamilton–Perelman proof of the Poincaré conjecture with kernel-checked, sorry-free theorems; validation by formal-mathematics experts would make it a machine-checked formalization of a Millennium Prize proof and a landmark of the AI-era formalization genre.

state: seedheat: lowuncertainty: highknownscott: lowai-assisted-formalization lean-formalization machine-checked-proofsqinz1yang

What is this?

The core claim here is first-party and uncorroborated by the supplied snippets: none of the web results mention qinz1yang or the Poincaré repo directly, so the repo's existence and its sorry-free, kernel-checked status rest entirely on the case's own evidence titles. What the snippets do establish is the surrounding regime: September 2026 is a dense stretch of AI-era formalization claims — Anthropic reported (Sept 4) Claude's Lean formalization of Fermat's Last Theorem (13M lines, ~29,500 lemmas, with Kevin Buzzard's independent review still pending), OpenAI reported (Sept 8) a Navier–Stokes singularity claim that remains independently unverified, and agentic autoformalization frameworks (Theo) are formalizing full research papers. NeoTeo's caveat frames the epistemics for this case: a Lean artifact makes the steps mechanically checkable but does not by itself establish that the formalized statement captures the intended mathematical problem or that the community accepts it — so the qinz1yang claim's significance hinges on exactly the expert-validation step the hypothesis flags. Who is behind the account is not established by the supplied material.

Why it matters to Scott

Scott's canon already prices this exact shape: Discussed Is Not Deployed and Mechanically Different Verifiers treat 'sorry-free, kernel-checked' as one verification class (step correctness) with statement fidelity and community acceptance as unevidenced higher rungs — precisely the split his Formalisation Bottleneck position predicts for the AI-formalization genre. This is a third genre instance after Fermat and Hopf, adding nothing new to argue until expert validation lands; if it does, it becomes the Millennium-Prize landmark the hypothesis flags and merits re-grounding and possibly a Discussed-Is-Not-Deployed-style writeup.

ip:framework.discussed-is-not-deployedip:concept.mechanically-different-verifiersip:concept.formalisation-bottleneckradar:concept.leanradar:concept.formal-mathematicsradar:concept.ai-assisted-mathematicsradar:anthropic-fermat-lean-formalizationradar:hopf-proof-codex-lean-formalization

queries asked of Scott's wikis

Lean formalization machine-checked proof assistant position
Anthropic Fermat FLT formalization episode
kernel verification as receipts for autonomous agent output
multi-agent shared state dependency graph coordination failures
statement fidelity vs step correctness eval validity
sorry-free axiom audit mechanical acceptance checks

Measured heat

now 0 pts/hpeak 13 pts/hcomments 0/hpeers p14momentum: steady2 platformsage 317h

points/hour across evidence · reading as of 2026-10-12 02:59:37.977291+11:00 · deterministic, not a model opinion

How the heat travelled

09-28 12:10 (minted)	⭐ origin echo-reconstructed	Repo claims sorry-free, kernel-checked Lean 4 formalizations including the Poincaré conjecture (topological and smooth versions), release v0 qinz1yang on github (echo) · attributed from hn.story.49876256 · published time unknown	—
09-28 11:14	first on hacker news · published · lag ?	Lean formalization of the Hamilton-Perelman proof of the Poincaré conjecture nill0	—
09-28 11:14	amplified on hacker news 👑	hn.story.49876256 nill0	peak 1 · 1 comments · 49% of case engagement
09-29 05:03	amplified on hacker news	hn.story.49888487 unexpectedtrap	peak 2 · 0 comments · 49% of case engagement
09-28 11:20	our radar first saw it · lag ?	discovery anchor: hn.story.49876256	—

pace: p35 vs 1188 stories at the 168h mark (now 317h old) — ahead of agentgate-signed-agent-receipts (1.3x), behind agentic-determinism-index (0.8x)

Evidence (3) — ⭐ canonical anchor

source	object	author	score	comments
🟧 hn	Lean formalization of the Hamilton-Perelman proof of the Poincaré conjecture Retrieved article excerpt Open article · Retrieved 2026-09-28T11:28:31.482476+00:00 # Differential Geometry in Lean 4 An ongoing Lean 4 library for differential geometry and geometric analysis, currently focused on Ricci flow. ## How to use Use DifferentialGeometry as an upstream dependency and build on its geometric-analysis infrastructure: ``` [[require]] name = "DifferentialGeometry" git = "https://github.com/qinz1yang/differential-geometry.git" rev = "v0.1.3" ``` Release `v0.1.3` is pinned to Lean and Mathlib `v4.33.1`. Import the full library with ``` import DifferentialGeometry ``` or a specific module, for example the scalar strong maximum principle: ``` import DifferentialGeometry.Analysis.Parabolic.MaximumPrinciple.Scalar.Strong ``` We aim to keep pace with Mathlib releases and update the pinned Mathlib version accordingly. ## Formalized theorems Each is `sorry`-free (axioms: `propext, Classical.choice, Quot.sound`). > These three are the standard axioms of Lean's core library — propositional extensionality, the axiom of choice, and quotient soundness — on which all of classical mathematics in Mathlib rests. `#print axioms` lists everything a theorem transitively assumes: a `sorry` would surface as `sorryAx`, and any ad-hoc axiom would be named. An output of exactly these three therefore certifies that the proof is fully kernel-checked, with no `sorry` and no assumptions beyond the classical foundations. - [Poincaré conjecture](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/ThreeManifold/Poincare.lean#L12) — every compact, Hausdorff, simply connected topological three-manifold without boundary is homeomorphic to the unit sphere $S^3 \subset \mathbb{R}^4$. The final statement uses only Lean/Mathlib concepts. The [smooth version](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Surgery/Skeleton/PoincareEndgame.lean#L103) gives a diffeomorphism for smooth three-manifolds. - [Finite-time extinction with surgery, simply connected case](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Surgery/Skeleton/PoincareEndgame.lean#L91) — every simply connected closed oriented smooth three-manifold, with any initial smooth Riemannian metric, admits a controlled finite surgery history ending in the empty manifold at a positive finite time. The [extinction structure](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Surgery/Topology/ControlledExtinction.lean#L14) records the initial metric identification and the empty terminal stage. - [Moise's theorem: compatible smooth structures in dimension three](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/PiecewiseLinear/Moise352Producer.lean#L33) — every compact Hausdorff topological three-manifold admits a smooth atlas compatible with its given topology. The development supplies [PL approximation](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/PiecewiseLinear/Moise352Producer.lean#L27) and [compact PL smoothing](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/PiecewiseLinear/Moise352Producer.lean#L30), providing the bridge from smooth to topological Poincaré. - [Perelman's canonical neighborhood theorem](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/CanonicalNeighborhood/HighCurvatureModelBounds.lean#L539) — in a Ricci flow on a closed connected oriented three-manifold over a finite time interval, every point of sufficiently large scalar curvature lies in a controlled neck, cap, positively curved compact component, or nearly round component. The development also gives [curvature-scale bounds for all mixed space-time curvature derivatives](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/CanonicalNeighborhood/HighCurvatureModelBounds.lean#L586). - [Compactness of ancient κ-solutions](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/CanonicalNeighborhood/HighCurvatureModelBounds.lean#L566) — three-dimensional ancient κ-solutions with fixed κ and basepoint scalar curvature normalized to one admit smoothly convergent pointed subsequences with an ancient κ-solution limit, together with [universal mixed curvature-derivative estimates](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/CanonicalNeighborhood/HighCurvatureModelBounds.lean#L579). - [Hamilton's compactness theorem](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Compactness/Limits/Hamilton.lean#L27) — complete connected pointed Ricci flows on a common open time interval, with uniform curvature bounds on compact time intervals and a uniform positive basepoint injectivity-radius bound at time zero, admit a smooth pointed Cheeger–Gromov–Hamilton convergent subsequence with a complete limit. - [Hamilton's theorem (1982)](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/DimensionThree/PositiveRicci/Hamilton.lean#L29) — a closed three-manifold admitting a positive-Ricci metric admits a constant-positive-sectional-curvature metric and is a spherical space form. - [Ricci flow short-time existence](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/ShortTime/Existence.lean#L34) — on every closed Riemannian manifold $(M, g\_0)$ the Ricci flow $\partial\_t g = -2,\mathrm{Ric}\_{g(t)}$ has a solution on some $[0, T)$ with $g(0) = g\_0$, jointly smooth in $(t, x)$ up to and including the initial time. Proved via the DeTurck's trick and a conjugating flow of the DeTurck vector field. - [Perelman's reduced-volume monotonicity](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/LGeometry/ReducedVolume/Basic.lean#L384) — along a Ricci flow on a closed connected manifold, the reduced volume is nonincreasing in backward time, built on the L-length minimizer, L-cut-locus, and reduced-Jacobian theory. - [Perelman's no local collapsing theorem](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/Noncollapsing/FiniteTime.lean#L33) — every smooth Ricci flow on a closed connected manifold over a finite time interval is uniformly κ-noncollapsed below any prescribed scale on curvature-controlled spacetime balls. - [Perelman's W-entropy monotonicity](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Entropy/W/Variation/Monotonicity.lean#L726) — along Ricci flow on a closed manifold, a positive conjugate-heat solution determines a W-entropy that is nonincreasing in backward time, with the [exact integral-square derivative formula](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Entropy/W/Variation/Monotonicity.lean#L281). - [Ricci–DeTurck flow short-time existence](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/ShortTime/DeTurck/InitialData.lean#L143) — the gauge-fixed, strictly parabolic flow behind the reduction: a solution whose chart-Gram entries are jointly smooth on the closed time slab, together with joint smoothness of the DeTurck vector field. - [Ricci-tensor naturality under diffeomorphisms](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Curvature/CurvatureOperator/Ricci/Naturality.lean#L250) — $\mathrm{Ric}\_{\Phi^\* g}(v, w) = \mathrm{Ric}\_g(d\Phi, v, d\Phi, w)$, the equivariance that transports the DeTurck solution back to a Ricci flow. - [Scalar-curvature evolution under Ricci flow](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Evolution/Scalar/IntrinsicDerivation.lean#L736). - [Hamilton–Ivey pinching estimate](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/DimensionThree/HamiltonIvey/MaximumPrinciple.lean#L5324) — the scalar-curvature lower bound and logarithmic pinching estimate for closed three-dimensional Ricci flows with an initial curvature-operator lower bound, together with an [asymptotic pinching estimate](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/DimensionThree/HamiltonIvey/MaximumPrinciple.lean#L5395). - [Shi's derivative estimates](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Estimates/Shi/TimeWeighted.lean#L20) — uniform curvature bounds and completeness of the initial metric give time-weighted bounds for every covariant derivative of curvature along Ricci flow. - [Hamilton's matrix Harnack inequality for Ricci flow](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/HamiltonHarnack/MatrixHarnack.lean#L10209) — the matrix Harnack quadratic is nonnegative on closed Ricci flows with nonnegative curvature operator. In dimension three, [nonnegative initial curvature operator suffices](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/HamiltonHarnack/MatrixHarnack.lean#L10247). - [Bonnet–Myers diameter bound](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Comparison/BonnetMyers/Diameter.lean#L506) — a positive Ricci lower bound forces a bounded diameter. - [Bochner formula](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Analysis/Elliptic/Regularity/Bochner/PolarisedLpSmooth.lean#L66) — the polarised, pointwise form. - [Weitzenböck identity](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Analysis/Elliptic/ConnectionLaplacian/Weitzenbock/IntegratedCovariantTensor.lean#L98) — the integrated $L^2$ form. - [Lichnerowicz eigenvalue bound](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Analysis/Elliptic/Lichnerowicz.lean#L598) on closed manifolds. - [Voss–Weyl divergence formula](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Analysis/Integration/DivergenceTheorem/Local/ChartInvariance.lean#L576) — the chart-invariant divergence. - [de Rham cohomology](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Tensor/Exterior/Cochain.lean#L72) — intrinsic differential forms with [nilpotent exterior derivative](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Tensor/Exterior/Basic.lean#L607), [graded Leibniz rule](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Tensor/Exterior/Leibniz.lean#L604), and [functorial pullback maps](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Tensor/Exterior/Cochain.lean#L159). - [Morse lemma](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/Morse/NormalForm/Manifold.lean#L950), the [no-critical-values theorem](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/Morse/RegularLevel/NoCriticalValues.lean#L187), and [single-critical-point cell attachment](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/Morse/Attachment/SmoothHandle.lean#L932), with [smooth handle-adjunction diffeomorphisms](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/Morse/Attachment/SublevelTransport.lean#L1033). - [Elliptic variable-coefficient	nill0	1	1
🟧 echo.github ⭐	Repo claims sorry-free, kernel-checked Lean 4 formalizations including the Poincaré conjecture (topological and smooth versions), release v0	qinz1yang	—	—
🟧 hn	Hamilton–Perelman's proof of Poincaré conjecture is claimed to be autoformalized	unexpectedtrap	2	0

source

object

author

score

comments

🟧 hn

Lean formalization of the Hamilton-Perelman proof of the Poincaré conjecture

Retrieved article excerpt

Open article · Retrieved 2026-09-28T11:28:31.482476+00:00

# Differential Geometry in Lean 4

An ongoing Lean 4 library for differential geometry and geometric analysis, currently focused on Ricci flow.

## How to use

Use DifferentialGeometry as an upstream dependency and build on its geometric-analysis infrastructure:

```
[[require]]
name = "DifferentialGeometry"
git = "https://github.com/qinz1yang/differential-geometry.git"
rev = "v0.1.3"
```

Release `v0.1.3` is pinned to Lean and Mathlib `v4.33.1`.

Import the full library with

```
import DifferentialGeometry
```

or a specific module, for example the scalar strong maximum principle:

```
import DifferentialGeometry.Analysis.Parabolic.MaximumPrinciple.Scalar.Strong
```

We aim to keep pace with Mathlib releases and update the pinned Mathlib version accordingly.

## Formalized theorems

Each is `sorry`-free (axioms: `propext, Classical.choice, Quot.sound`).

> These three are the standard axioms of Lean's core library — propositional extensionality, the axiom of choice, and quotient soundness — on which all of classical mathematics in Mathlib rests. `#print axioms` lists everything a theorem transitively assumes: a `sorry` would surface as `sorryAx`, and any ad-hoc axiom would be named. An output of exactly these three therefore certifies that the proof is fully kernel-checked, with no `sorry` and no assumptions beyond the classical foundations.

- [Poincaré conjecture](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/ThreeManifold/Poincare.lean#L12) — every compact, Hausdorff, simply connected topological three-manifold without boundary is homeomorphic to the unit sphere $S^3 \subset \mathbb{R}^4$. The final statement uses only Lean/Mathlib concepts. The [smooth version](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Surgery/Skeleton/PoincareEndgame.lean#L103) gives a diffeomorphism for smooth three-manifolds.
- [Finite-time extinction with surgery, simply connected case](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Surgery/Skeleton/PoincareEndgame.lean#L91) — every simply connected closed oriented smooth three-manifold, with any initial smooth Riemannian metric, admits a controlled finite surgery history ending in the empty manifold at a positive finite time. The [extinction structure](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Surgery/Topology/ControlledExtinction.lean#L14) records the initial metric identification and the empty terminal stage.
- [Moise's theorem: compatible smooth structures in dimension three](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/PiecewiseLinear/Moise352Producer.lean#L33) — every compact Hausdorff topological three-manifold admits a smooth atlas compatible with its given topology. The development supplies [PL approximation](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/PiecewiseLinear/Moise352Producer.lean#L27) and [compact PL smoothing](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/PiecewiseLinear/Moise352Producer.lean#L30), providing the bridge from smooth to topological Poincaré.
- [Perelman's canonical neighborhood theorem](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/CanonicalNeighborhood/HighCurvatureModelBounds.lean#L539) — in a Ricci flow on a closed connected oriented three-manifold over a finite time interval, every point of sufficiently large scalar curvature lies in a controlled neck, cap, positively curved compact component, or nearly round component. The development also gives [curvature-scale bounds for all mixed space-time curvature derivatives](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/CanonicalNeighborhood/HighCurvatureModelBounds.lean#L586).
- [Compactness of ancient κ-solutions](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/CanonicalNeighborhood/HighCurvatureModelBounds.lean#L566) — three-dimensional ancient κ-solutions with fixed κ and basepoint scalar curvature normalized to one admit smoothly convergent pointed subsequences with an ancient κ-solution limit, together with [universal mixed curvature-derivative estimates](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/CanonicalNeighborhood/HighCurvatureModelBounds.lean#L579).
- [Hamilton's compactness theorem](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Compactness/Limits/Hamilton.lean#L27) — complete connected pointed Ricci flows on a common open time interval, with uniform curvature bounds on compact time intervals and a uniform positive basepoint injectivity-radius bound at time zero, admit a smooth pointed Cheeger–Gromov–Hamilton convergent subsequence with a complete limit.
- [Hamilton's theorem (1982)](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/DimensionThree/PositiveRicci/Hamilton.lean#L29) — a closed three-manifold admitting a positive-Ricci metric admits a constant-positive-sectional-curvature metric and is a spherical space form.
- [Ricci flow short-time existence](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/ShortTime/Existence.lean#L34) — on every closed Riemannian manifold $(M, g\_0)$ the Ricci flow $\partial\_t g = -2,\mathrm{Ric}\_{g(t)}$ has a solution on some $[0, T)$ with $g(0) = g\_0$, jointly smooth in $(t, x)$ up to and including the initial time. Proved via the DeTurck's trick and a conjugating flow of the DeTurck vector field.
- [Perelman's reduced-volume monotonicity](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/LGeometry/ReducedVolume/Basic.lean#L384) — along a Ricci flow on a closed connected manifold, the reduced volume is nonincreasing in backward time, built on the L-length minimizer, L-cut-locus, and reduced-Jacobian theory.
- [Perelman's no local collapsing theorem](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Perelman/Noncollapsing/FiniteTime.lean#L33) — every smooth Ricci flow on a closed connected manifold over a finite time interval is uniformly κ-noncollapsed below any prescribed scale on curvature-controlled spacetime balls.
- [Perelman's W-entropy monotonicity](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Entropy/W/Variation/Monotonicity.lean#L726) — along Ricci flow on a closed manifold, a positive conjugate-heat solution determines a W-entropy that is nonincreasing in backward time, with the [exact integral-square derivative formula](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Entropy/W/Variation/Monotonicity.lean#L281).
- [Ricci–DeTurck flow short-time existence](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/ShortTime/DeTurck/InitialData.lean#L143) — the gauge-fixed, strictly parabolic flow behind the reduction: a solution whose chart-Gram entries are jointly smooth on the closed time slab, together with joint smoothness of the DeTurck vector field.
- [Ricci-tensor naturality under diffeomorphisms](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Curvature/CurvatureOperator/Ricci/Naturality.lean#L250) — $\mathrm{Ric}\_{\Phi^\* g}(v, w) = \mathrm{Ric}\_g(d\Phi, v, d\Phi, w)$, the equivariance that transports the DeTurck solution back to a Ricci flow.
- [Scalar-curvature evolution under Ricci flow](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Evolution/Scalar/IntrinsicDerivation.lean#L736).
- [Hamilton–Ivey pinching estimate](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/DimensionThree/HamiltonIvey/MaximumPrinciple.lean#L5324) — the scalar-curvature lower bound and logarithmic pinching estimate for closed three-dimensional Ricci flows with an initial curvature-operator lower bound, together with an [asymptotic pinching estimate](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/DimensionThree/HamiltonIvey/MaximumPrinciple.lean#L5395).
- [Shi's derivative estimates](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/Estimates/Shi/TimeWeighted.lean#L20) — uniform curvature bounds and completeness of the initial metric give time-weighted bounds for every covariant derivative of curvature along Ricci flow.
- [Hamilton's matrix Harnack inequality for Ricci flow](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/HamiltonHarnack/MatrixHarnack.lean#L10209) — the matrix Harnack quadratic is nonnegative on closed Ricci flows with nonnegative curvature operator. In dimension three, [nonnegative initial curvature operator suffices](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Flow/RicciFlow/HamiltonHarnack/MatrixHarnack.lean#L10247).
- [Bonnet–Myers diameter bound](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Geometry/Comparison/BonnetMyers/Diameter.lean#L506) — a positive Ricci lower bound forces a bounded diameter.
- [Bochner formula](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Analysis/Elliptic/Regularity/Bochner/PolarisedLpSmooth.lean#L66) — the polarised, pointwise form.
- [Weitzenböck identity](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Analysis/Elliptic/ConnectionLaplacian/Weitzenbock/IntegratedCovariantTensor.lean#L98) — the integrated $L^2$ form.
- [Lichnerowicz eigenvalue bound](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Analysis/Elliptic/Lichnerowicz.lean#L598) on closed manifolds.
- [Voss–Weyl divergence formula](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Analysis/Integration/DivergenceTheorem/Local/ChartInvariance.lean#L576) — the chart-invariant divergence.
- [de Rham cohomology](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Tensor/Exterior/Cochain.lean#L72) — intrinsic differential forms with [nilpotent exterior derivative](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Tensor/Exterior/Basic.lean#L607), [graded Leibniz rule](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Tensor/Exterior/Leibniz.lean#L604), and [functorial pullback maps](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Tensor/Exterior/Cochain.lean#L159).
- [Morse lemma](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/Morse/NormalForm/Manifold.lean#L950), the [no-critical-values theorem](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/Morse/RegularLevel/NoCriticalValues.lean#L187), and [single-critical-point cell attachment](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/Morse/Attachment/SmoothHandle.lean#L932), with [smooth handle-adjunction diffeomorphisms](https://github.com/qinz1yang/differential-geometry/blob/main/DifferentialGeometry/Topology/Morse/Attachment/SublevelTransport.lean#L1033).
- [Elliptic variable-coefficient

nill0

🟧 echo.github ⭐

Repo claims sorry-free, kernel-checked Lean 4 formalizations including the Poincaré conjecture (topological and smooth versions), release v0

qinz1yang

—

🟧 hn

Hamilton–Perelman's proof of Poincaré conjecture is claimed to be autoformalized

unexpectedtrap

Interpretation history

2026-09-29T05:24:31Z
The 'new' evidence is a second HN submission of the same first-party claim at negligible traction (2 points, 0 comments) — repetitive amplification, not independent corroboration, so the case's meaning is unchanged: a real, checkable artifact whose significance still hinges entirely on the absent expert-validation step. Only unexplored lead is nill0's link to an ayushkhaitan343 x.com post, which could name a validator or origin.
2026-09-29T05:23:22Z
evidence attached: hn.story.49888487 — shared external link with case evidence
2026-09-28T12:18:53Z
grounded: known/low — Scott's canon already prices this exact shape: Discussed Is Not Deployed and Mechanically Different Verifiers treat 'sorry-free, kernel-checked' as one verifica
2026-09-28T12:10:01Z
case created — Checkable first-party artifact claiming formalization of a Millennium-Prize proof — a distinct episode in the tracked Fermat/Hopf formalization genre, not an attach to either.

Decision trace

09-29 15:24repriceThe 'new' evidence is a second HN submission of the same first-party claim at negligible traction (2 points, 0 comments) — repetitive amplification, not independent corroboration, so the cas
09-29 15:23attachshared external link with case evidence
09-29 15:20propose_attachshared external link with case evidence
09-28 22:18groundScott's canon already prices this exact shape: Discussed Is Not Deployed and Mechanically Different Verifiers treat 'sorry-free, kernel-checked' as one verification class (step correctn
09-28 22:10createCheckable first-party artifact claiming formalization of a Millennium-Prize proof — a distinct episode in the tracked Fermat/Hopf formalization genre, not an attach to either.