Post

@booleananalysis.bsky.social

Cayden Codel & Noah Singer have formalized in Lean the climactic theorems of the Kaufman-Oppenheim paper that shows the A_3-type coset complex HDXs are cosystolic expanders! (I.e., Sec. 7.2 of arxiv.org/abs/1907.01259) It's a warmup for the main project...

arxiv.orgarxiv.org

9/1/25, 10:51 pm1 repost9 likes

Ryan O'Donnell

@booleananalysis.bsky.social

9 Jan 2025

... which is to formalize the analogous theorems for the B_3 case (specifically, Sec. 8 of my recent paper with Noah: arxiv.org/pdf/2411.05916). The proofs there are 70 pages of Noah solving the word problem by hand. So it will be nice to have a computer check his work -- a team is being assembled!

arxiv.orgarxiv.org