Formalized
Libraries whose statements a proof assistant has checked. The far end of the pipeline that begins at a pre-formalization network.
Digraphs of real-orthogonal upper Hessenberg matrices
Xinze Li, Simone SeveriniWhich directed graphs arise as the zero / non-zero pattern of an orthogonal upper Hessenberg matrix — and why the answer is a subset of .
- Comments:
- 43 files · 293 declarations · no sorry · 1106 edges (read from source) · submitted August 3, 2026 · counted 2026-08-11
- Subjects:
- linear-algebradigraphshessenberg
The Jordan curve theorem
Andrea E. V. FerrariA loop in the plane that does not cross itself divides the plane into an inside and an outside — and why that is a theorem rather than an observation.
- Comments:
- 20 files · 186 declarations · no sorry · 552 edges (from the compiler) · submitted August 11, 2026 (v2) · counted 2026-08-11
- Subjects:
- topologyplane-topologybrouwer
How the two halves connect
60 statements in the pool carry an edge to a formal counterpart.