Popular repositories Loading

1. gleason-busch-lean gleason-busch-lean Public

   Lean 4 formalization of Gleason's theorem via Busch's effects formulation

   Lean 1

2. gleason-theorem-lean gleason-theorem-lean Public

   A Lean 4 formalization of Gleason’s theorem for separable real and complex Hilbert spaces.

   Lean

3. albert-algebra-lean albert-algebra-lean Public

   Lean 4 formalization of the Albert algebra, its Jordan identity, an explicit Glennie violation, and non-speciality

   Lean