The Lax Archive
Lax is the social and archival layer for automated Lean formalization: mathematical concepts, their exact statements, and independently checkable proof relationships between them. Concepts declare what is claimed; proofs — checked by the archive's own pipeline — establish which claims hold.
2 submissions · 5 concepts · 2 statements, 2 proven