On the Last Kervaire Invariant Problem

by Weinan Lin, Guozhen Wang, and Zhouli Xu

This is a Lean 4 formalization project for the paper On the Last Kervaire Invariant Problem, which proves that framed manifolds of Kervaire invariant one exist in dimension 126.

• Blueprint
  Interactive blueprint with dependency graph and review system
• Blueprint as PDF
  Downloadable PDF version of the blueprint
• Lean API Docs
  Auto-generated documentation for the Lean formalization
• Source Code
  GitHub repository