Popular repositories Loading

1. godel-loeb godel-loeb Public

   Lean 4 formalization of a modal-axiomatic Gödel-Löb provability-logic substrate and Löb's theorem.

   Lean 2

2. cencov-petz cencov-petz Public

   Lean 4 proof of the finite Čencov–Petz uniqueness theorem: continuous monotone metrics on finite probability simplexes are scalar multiples of Fisher information.

   Lean

3. compact-spectral compact-spectral Public

   Lean 4 proof of the spectral theorem for compact self-adjoint operators: a Hilbert basis of eigenvectors exists.

   Lean

4. rellich-kondrachov rellich-kondrachov Public

   Lean 4 proof of Rellich–Kondrachov: the H¹ to L² Sobolev embedding is compact on compact Riemannian manifolds.

   Lean

5. abenenson.github.io abenenson.github.io Public

   Personal site — writing, papers, projects

   HTML

6. channel-capacity channel-capacity Public

   Lean 4 formalization of uniqueness of capacity-achieving priors for Markov kernels

   Lean