Edward W. AyersI'm an accomplished mathematician and software engineer with expertise in automated reasoning, computer vision, and functional programming. I'm a quick learner, a generalist, and an expert programmer in Python and TypeScript.
(contact@) edayers.com , GitHub, LinkedIn.
Ph.D. in Mathematics, University of Cambridge 2016-2021I studied automated reasoning under Fields Medallist Tim Gowers and Mateja Jamnik. I focussed on methods for finding mathematical proofs that are as close as possible to what a human would produce (video). I also built the 'ProofWidgets' UI framework for Lean 3 used by over 200 mathematicians. The thesis is published as a custom website.
Mathematics Tripos Part III, University of Cambridge 2015-2016Logic, category theory, quantum information. Pass with merit.
Natural Sciences Tripos, University of Cambridge2012-2015Specialised in Physics, first class honours and best essay award.
Cofounder, HitSave.io 2022-presentDesigned and built open-source collaborative infrastructure tooling for data scientists. Conducted market research and customer discovery to understand the needs and pain points of potential users.
Postdoctoral Researcher, Carnegie Mellon University2022I worked in the Hoskinson Center for Formal Mathematics led by Jeremy Avigad. I worked on the user interface framework for the Lean 4 theorem prover and various collaborations in AI for theorem proving (see projects, publications).
Research Scientist, Five AI2020-2022I worked on verification of neural networks for autonomous vehicles in the Scene Understanding Team. Our team maintained a suite of machine learning models, datasets and infrastructure for the company. I primarily worked on object detectors: RetinaNet, Faster R-CNN and novel and bespoke, in-house architectures.
Teaching, University of Cambridge 2016-2020I supervised undergraduates (tutoring small groups) in first-year physics and third-year quantum information for mathematicians.
Internship, ARM Ltd.2014Designed, wrote and tested a hardware driver for power control of a System-on-Chip in C++. Implemented a testbench for the driver in Verilog.
Lean Prover 2020-presentI am a contributor to both Lean 3 and Lean 4 theorem provers, led by Leo de Moura and Jeremy Avigad. I built the interactive user interface system for Lean 3 and I am a main contributor to the corresponding Lean 4 port. I contribute documentation, bugfixes and support.
VR teaching, Isaac Physics2015Wrote the Isaac 3D virtual reality app for visualising physics problems using Google Cardboard. Written in Unity, I wrote custom shaders and mesh generation algorithms for visualising the orbitals of an atom.
- With Zhangir Azerbayev, built Lean chatautoformalization VSCode extension for Lean. Also Mathlib-search, a GPT-3-powered search engine for theorems in Lean.
- Created KaTeX-react, a fork of KaTeX using React.
- With Eric Hanson, built Arχiv-Search, a full-text search service for the Arχiv.
- Interactive notes for the Part III Hypergraph Games course.
- MoJ Online Courts Hackathon 2017, winning 'coolest tech' award.
- Wrote a dictionary app for Windows Phone 7, a top-10 app with millions of downloads.
PublicationsLast updated 2023-03-05
- Query-based Hard-Image Retrieval for Object Detection at Test Time AAAI 2023
- A Graphical User Interface Framework for Formal Verification ITP 2021 (slides)
- PaRoT: A Practical Framework for Robust Deep Neural Network Training NASA Formal Methods 2020
- A human-oriented term rewriting system KI 2019
- Is Schrödinger’s Cat Real? Exploring Quantum Bayesianism with Monoidal Categories Part III essay.