Euler's theorem on Eulerian circuits and trails, and Petersen's 2-factor theorem
A Lean 4 / Mathlib formalization of the classical characterization of Eulerian graphs and of Petersen's 2-factor theorem, for finite simple graphs. (1) Euler–Hierholzer: a finite connected graph has an Eulerian circuit if and only if every vertex has even degree, and the circuit can start at any prescribed vertex. (2) Eulerian trails: a finite connected graph has an Eulerian trail if and only if it has 0 or 2 vertices of odd degree; when the odd vertices are exactly a and b, there is an Eulerian trail from a to b. (3) Eulerian orientations: if every degree is even, the edges can be oriented…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-16-000016
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000016/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000016/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'