Colby Austin Brown

colbyabrown at math dot ucdavis dot edu

• preprint: An almost linear time algorithm testing whether the Markoff graph modulo p is connected
• libbgs on github
• libbgs Rustdocs

• Talks on Lean

  These talks are Lean files meant to be presented as slideshows. Portions of the talk are meant to be filled in real-time during the presentation.
  • Predicate Logic in Dependent Type Theory
  • A Short Proof that 0 /= 1

• Formalization of "Sheaves in Geometry and Logic" by Mac Lane and Moerdijk

  Code on Github More code in my mathlib fork (see Mathlib.CategoryTheory.Topos) Current progress:
  • Chapter 1: All exercises complete
  • Chapter 4:
    • Theorem 2.1: Every topos has exponentials. Complete
    • Theorem 5.1: The power functor has a left adjoint. Complete
    • Theorem 5.3: The power functor is monadic. In progress