PeopleofSuperintelligence

Researcher

Jireh Loreaux

Jireh Loreaux is an associate professor of mathematics at Southern Illinois University Edwardsville and a maintainer of Mathlib, the library of formalized mathematics for the Lean theorem prover. Trained in operator theory at the University of Cincinnati, he earned a BA in 2010 and a PhD in 2016 with a dissertation on diagonals of operators supervised by Gary Lynn Weiss. He began formalizing mathematics in Lean in 2018 and contributing to Mathlib in 2021, and with Anatole Dedecker he completed Mathlib's non-unital continuous functional calculus in May 2024. Their January 2025 paper described the first formalization of the continuous functional calculus in any proof assistant. In 2025 and 2026, he co-organized the Lean Together meetings, whose 2026 program featured Aristotle, an AI theorem prover trained on Lean proofs.

Now at
Southern Illinois University Edwardsville

Timeline

  1. 2010–2016

    Degrees at Cincinnati

    He earns a BA with honors in mathematics at the University of Cincinnati in 2010 and a PhD in operator theory and operator algebras there in 2016. His dissertation, "Diagonals of operators: Majorization, a Schur-Horn theorem and zero-diagonal idempotents," is supervised by Gary Lynn Weiss, with whom he publishes a Schur–Horn theorem for positive compact operators in the Journal of Functional Analysis in 2015.

  2. 2018–2021

    From Lean to Mathlib

    He begins formalizing mathematics in the Lean proof assistant in 2018 and starts contributing to Mathlib in 2021.

  3. By 2021

    Assistant professor at SIUE

    By 2021, he is an assistant professor of mathematics at Southern Illinois University Edwardsville, working on operator theory, operator algebras and matrix theory. His 2021 preprints include a study of K1-injectivity of the Paschke dual algebra with Ping Wong Ng and Arindam Sutradhar.

  4. May 2024

    Non-unital functional calculus

    In May 2024, he and Anatole Dedecker complete the development of Mathlib's non-unital continuous functional calculus, including the instances for C*-algebras that had been missing.

  5. January 2025

    The continuous functional calculus in Lean

    In January 2025, he and Dedecker post "The continuous functional calculus in Lean" to arXiv. The paper describes the first formalization of the continuous functional calculus in any proof assistant, a basic construction in the theory of C*-algebras, and their code is already merged into Mathlib.

  6. 2025–2026

    Organizing Lean Together

    He co-organizes Lean Together 2025 with Riccardo Brasca and Kevin Buzzard in January 2025, and Lean Together 2026 with Rémy Degenne, Markus Himmel and Patrick Massot in January 2026. The annual virtual meeting gathers users and developers of Lean and Mathlib, and its 2026 program includes a talk by Alex Best of Harmonic on Aristotle, an AI theorem prover trained via reinforcement learning on Lean proofs.

  7. May 2026

    Operator algebras at ICERM

    In May 2026, he speaks at ICERM's Techniques and Tools for the Formalization of Analysis event on the obstacles and opportunities in formalizing operator algebras, a field still at an early stage of formalization. His talk highlights places where bespoke tactics may be particularly effective.

  8. As of October 2026

    Associate professor and Mathlib maintainer

    He is an associate professor of mathematics in the Department of Mathematics and Statistics at Southern Illinois University Edwardsville. As a Mathlib maintainer, he is one of the people with the power to give final approval to pull requests to the library.

Career

  1. Since 2021Southern Illinois University EdwardsvilleAssistant professor of mathematics

Education

  1. 2016University of CincinnatiPhD
  2. 2010University of CincinnatiBA

From the biography.

  1. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other universityIncludes University of Cincinnati. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other university. We compare doctorate and 5+ year employment links, career timing and current workplaces for 187 major-prize and 1,111 best-paper winners.
  2. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes University of Cincinnati. We estimate where the people shaping AI studied and where their careers led. Massachusetts Institute of Technology leads with 467 former students, including 291 recorded doctorates.
  3. The company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes University of Cincinnati. We estimate where the people shaping AI worked when their most-cited papers appeared: the company share was 31% in 2020–2024 and 8% in 1970–1974, and Google led all organizations in 2020–2024.
  4. Google had the most people shaping AI every year from 2014 to 2025Our estimates of which organizations employed the most people shaping AI each year from 1955 to 2025, tracing the shift from university labs to companies.

Colleagues

People named in this biography, and people with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Jireh Loreaux yet. Send us a free-licensed photo.

  1. JIREH LOREAUX siue.edu. Checked 20 October 2026.
  2. Jireh Loreaux - The Mathematics Genealogy Project mathgenealogy.org. Checked 20 October 2026.
  3. Mathlib maintainers leanprover-community.github.io. Checked 20 October 2026.
  4. This month in Mathlib (May 2024) | Lean community blog leanprover-community.github.io. Checked 20 October 2026.
  5. [2501.15639] The continuous functional calculus in Lean arxiv.org. Checked 20 October 2026.
  6. Lean Together 2025 researchseminars.org. Checked 20 October 2026.
  7. Lean Together 2026 | A meeting all about Lean leanprover-community.github.io. Checked 20 October 2026.
  8. Aristotle, an AI theorem prover using Lean researchseminars.org. Checked 20 October 2026.
  9. Obstacles and opportunities in the formalization of operator algebras mathinstitutes.org. Checked 20 October 2026.
  10. Faculty & Staff - Mathematics & Statistics | SIUE siue.edu. Checked 20 October 2026.