Jonathan Llovet is a software architect and computer scientist building tools to study the deep structural relationships among formal logic, computation, and mathematics. He is the creator of ProofGraph, a research project and open-source platform that applies network science and spectral graph theory to the dependency graphs of formalized mathematics.

His path to this work began at St. John’s College, where a study of Jacob Klein’s Greek Mathematical Thought and the Origin of Algebra raised foundational questions about the nature of mathematics and computation. Eight years of professional experience in cybersecurity and software architecture followed, including dataflow analysis and taint tracking techniques that directly inform ProofGraph’s approach to proof-theoretic property propagation.

ProofGraph builds on the Curry-Howard-Lambek correspondence to treat formalized mathematics libraries as complex networks whose structure can be studied empirically. The project extracts declaration-level dependency graphs from Lean 4 projects, computes proof-theoretic properties (constructivity, computability, axiom dependence), and applies methods from network science, including community detection, centrality analysis, and structural hole identification, to characterize how verified mathematical knowledge is organized.