E.W.Ayers

Edward W. Ayers

I'm a 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.

Education

Ph.D. in Mathematics, University of Cambridge 2016-2021

I studied automated reasoning under 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-2016

Logic, category theory, quantum information. Pass with merit.

Natural Sciences Tripos, University of Cambridge2012-2015

Specialised in Physics, first class honours and best essay award.

Experience

Founding engineer, Cogna 2023-present

AI for software synthesis.

Postdoctoral Researcher, Carnegie Mellon University2022

I 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-2022

I 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 bespoke, in-house architectures.

Teaching, University of Cambridge 2016-2020

I supervised undergraduates (tutoring small groups) in first-year physics and third-year quantum information for mathematicians.

Internship, ARM Ltd.2014

Designed, wrote and tested a hardware driver for power control of a System-on-Chip in C++. Implemented a testbench for the driver in Verilog.

Projects

Cofounder, HitSave.io 2022-2023

Designed and built open-source collaborative infrastructure tooling for data scientists.

Lean Prover 2020-present

I 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 Physics2015

Wrote 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.

Other projects

Publications

Last updated 2023-08-22

Primary author

Contributor