Kelly J. Davis

Kelly J. Davis

Machine learning and speech technology. Former Co-Founder/CEO of Coqui (TTS), Manager of Mozilla's ML group (Deep Speech, Common Voice). Ph.D. Physics (Rutgers), B.S. Mathematics (MIT).

Blog posts

2026

Spectral Theorem for Unbounded, Self-Adjoint Operators

283 minute read

Published:

Here we will state and prove the Spectral Theorem for Unbounded, Self-Adjoint Operators. This theorem extends the Spectral Theorem for Bounded, Self-Adjoint Operators to the small handful of genuinely unbounded self-adjoint operators that do arise in AQFT — the momentum operator on Minkowski space is a standard example — even though the large majority of operators of interest there, local observables in particular, are bounded. It is a prerequisite for handling these unbounded operators within the rest of the AQFT work that motivated this series.

Local Isometric Invariant States

45 minute read

Published:

This blog post introduces the notion of “isometric invariant states” in Algebraic Quantum Field Theory (AQFT) in Minkowski spacetime (a theory defined in Unpacking the Haag Kastler Axioms) and also does the same for AQFT in Lorentzian spacetime (a theory defined in Haag Kastler Axioms in Curved Spacetime). Such “isometric invariant states” capture the physics of quantum systems that are invariant under isometries of spacetime.

GNS Construction Theorem

23 minute read

Published:

In this blog post we will state and prove the GNS Construction Theorem, which we make extensive use of in subsequent blog posts.

Unpacking the Haag Kastler Axioms

40 minute read

Published:

The aim of this blog post is to “sharpen” the statement of the Haag Kastler axioms (Haag and Kastler). As originally presented they were revolutionary. However, several small details were left under-specified. This blog post will hopefully clarify some of these details.

Gödel’s Poetry: AI, Lean4 Prover

5 minute read

Published:

Gödel’s Poetry (PDF) is a Lean 4 system that combines specialized language models for proof generation with recursive decomposition of difficult theorems into simpler entailing propositions, coordinated through a multi-agent architecture as in the arXiv manuscript. Proof verification runs through the Kimina Lean Server; when direct proof generation (with verifier-guided self-correction in the style of Goedel-Prover-V2) does not yield a closed proof, the stack falls back to RAG-based theorem retrieval, proof sketching with sorry placeholders in explicit have obligations, AST-based extraction of those subgoals, recursive proof of each proposition, and finally proof reconstruction that substitutes verified sub-proofs back into the parent sketch.