About

I am Kelly J. Davis. My current, primary interest is the application of deep learning to formal theorem proving—systems like Gödel-Prover-V2, DeepSeek-Prover-V2, the Kimina-Prover preview, and my own Gödel’s Poetry. I see this as the way forward for mathematics: it will transform how we author articles, write and check proofs, and explore mathematical structures.

Beyond mathematics, I see the same direction for physics. Physics, starved for revolutionary (not merely evolutionary) experimental results, relies ever more on theory—theory whose foundations are often less solid than those of mathematics (see, for example, the introduction of Talagrand’s What is a Quantum Field Theory). Axiomatic approaches—such as the Haag–Kastler axioms or locally covariant quantum field theory (LCQFT)—strengthen these foundations and allow definitive, formal theorems to be derived, by hand or with deep-learning theorem provers. Such theorems can then be checked or refuted observationally, and provers can be used to iterate quickly over alternative axiomatizations.

Background: I was Co-Founder and CEO of Coqui (2020–2023), building open-source TTS (e.g. XTTS, Tortoise) and Coqui Studio. Before that I managed the Machine Learning group at Mozilla (2016–2020), where we built Deep Speech, Common Voice, and Mozilla TTS, and led technical work on grants such as Bergamot (NMT), Papa Reo (te reo Māori), and SIFIS-Home (IoT). I have also held technical and leadership roles at So1, forty.to, mentalimages/NVIDIA, Max-Planck-Institut für Gravitationsphysik, and Semantic Edge.

Education: Ph.D. (all but defense) in Physics, Rutgers University; B.S. in Mathematics, MIT.

Location: Berlin, Germany.