Open Research Index

Petersen's theorem

Juan Pablo Traverso Gianini

Palomar Registrypalomar/PALOMAR-2026-10-16-000004Oct 16, 2026math.COscore 0

A Lean 4 / Mathlib formalization of Petersen's theorem: a finite 3-regular graph in which no edge is a bridge has a perfect matching; moreover, every edge of such a graph lies in some perfect matching. Both statements are derived from Tutte's theorem (in Mathlib) by counting the edges that leave the odd components.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-16-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000004/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-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'