Ellipsoid fitting & GaussianAnalysisPublic source ↗

Mathematics formalized in Rocq

The paper.
The library.

The paper explains results about fitting ellipsoids to random points. The library collects the general mathematics developed along the way, so those proofs can be understood and reused in other problems.

01 / The paper

Ellipsoid fitting

The mathematical problem, the main theorem and the new results on conditioning, dependent coordinates and translated samples.

  • Understand the geometric ideas and explore the condition-number curve.
  • Read the hypotheses, proof outline and mathematical notes.
  • Find the precise statements and proofs in the released source.
Read about the paper →

Exposition updated 27 October 2026.

02 / The library

GaussianAnalysis

A reusable library of Gaussian probability, comparison inequalities, matrix theory, concentration, Fourier analysis and convex geometry.

  • The overview presents the nine subject areas of the release, 128 modules in all, with a representative result for each area.
  • The overview links to the Rocq sources of the release and to the library’s table of main results, with names and informal statements.
  • The declaration browser offers search, full Rocq signatures and links between declarations, for an earlier version of the library.
Read the library overview →Declaration browser: phase 12 snapshot of 13 October 2026 →

The overview covers the release tagged shifted (24 October 2026). The declaration browser was generated at commit 9046883 of phase 12 and covers its 94 library modules.