Hello, I am Edward Ayers.

I am currently an ML consultant for Bloop.

• I have completed a PhD at the University of Cambridge in interactive theorem proving at DPMMS. Supervised by W.T. Gowers and Mateja Jamnik. The thesis can be found here.
• I worked as a post-doctoral researcher at Carnegie Mellon University at the Hoskinson Center for Formal Mathematics led by Jeremy Avigad.
• I contribute to Lean 4, a proof assistant, mainly creating user interfaces for it.Wojciech Nawrocki and I are creating a WidgetKit library for Lean 4 users to create their own widgets without needing to write any JavaScript. Previously, I built the 'ProofWidgets' UI framework for community fork of the Lean 3 proof assistant. A paper on ProofWidgets was published at ITP 2021 (Paper, talk slides).
• I was a research scientist at Five AI 2020-2022, working on verification for ML in computer vision. While there I contributed to a couple of research papers: PaRoT presented at NASA Formal Methods 2020. Query-based Hard-Image Retrieval for Object Detection at Test Time has been accepted to AAAI 2023.
• A human-oriented term rewriting system was published at KI 2019.

You can email me with contact@$THIS_DOMAIN.

Social media accounts: GitHub, Goodreads, Lichess, Manifold, Twitter, LinkedIn. I make tracks.