PeopleofSuperintelligence

Researcher

Emilio Jesús Gallego Arias

Emilio Jesús Gallego Arias is a computer scientist who develops software for formal mathematics and interactive theorem proving. He studied computer science at Madrid's Technical University and held research posts at the University of Pennsylvania, MINES ParisTech, Inria and CNRS. His work includes jsCoq, a browser based environment for Coq, and NLIR, a 2024 study that uses a language model agent to interact with a proof assistant. Since December 2025, he is a Senior Research Engineer at Lean FRO, where he works on a collaborative Lean 4 workbench and organizes the Lean Paris Meetup.

Links
Website, X and GitHub

Timeline

  1. 1998–2012

    Informatics Olympiads and a PhD

    From Las Pedroñeras in Cuenca, Spain, he places ninth in the first two Spanish Olympiads in Informatics while in high school. He studies computer science at Madrid's Technical University from 1998, joins the Babel research group, and earns a degree with honors in 2005, a European master's in computational logic with honors in 2007, and a computer science PhD with Jim Lipton and Julio Mariño in 2012; his thesis is Relational and Allegorical Semantics for Constraint Logic Programming.

  2. 2012–2014

    Privacy verification at Penn

    At the University of Pennsylvania's programming languages group, he works as a postdoctoral researcher with Benjamin Pierce from 2012 to 2014. In 2014, he coauthors a preprint on approximate relational refinement types for mechanism design and differential privacy.

  3. 2014–2019

    jsCoq and proof development

    At MINES ParisTech, he works with Pierre Jouvelot as a postdoctoral researcher from 2014 to 2019 on Faust Everywhere and universal proof development environments. In 2017, he coauthors jsCoq, a browser based environment for the Coq interactive proof assistant.

  4. 2019–2024

    LLMs and natural language in proofs

    He joins Inria as a Starting Researcher in its π³ team in 2019, working on unified environments for large scale verification and collaborative verified mathematical documents. In 2024, he coauthors NLIR, a study that uses a large language model agent and natural language to interact with the Rocq proof assistant.

  5. 2025

    CNRS and the MALINCA project

    At CNRS, he works as a Research Engineer in the π³ team on MALINCA in 2025, a project to bridge the linguistic gap between mathematicians and machines.

  6. Since December 2025

    Lean FRO and the Paris meetup

    He joins Lean FRO as a Senior Research Engineer in December 2025, working on a collaborative mathematical workbench for Lean 4. In April 2026, he organizes the inaugural Lean Paris Meetup at Mines Paris – PSL, where researchers, developers, mathematicians and industry practitioners gather around Lean, rigorous mathematical proofs and verified software.

  1. Google had the most people shaping AI every year from 2014 to 2025Our estimates of which organizations employed the most people shaping AI from 1961 to 2025, with a year-by-year chart.
  2. The United States employs an estimated 53% of people in our data with a known employment countryOur estimates of where AI careers are concentrated now and how countries’ shares of dated positions changed over time.
  3. 46% of living people in our data with known birth and employment countries work outside their birth countryOur estimate of cross-border careers in AI, from country of birth and the country of each current organization.
  4. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionOur estimates of where the people shaping AI studied and where their careers led, from education records in cited biographies.

Sources and credits

Photo: We have no published photo of Emilio Jesús Gallego Arias yet. Send us a free-licensed photo.

  1. About - Emilio Jesús Gallego Arias x80.org. Checked 19 October 2026.
  2. Relational and Allegorical Semantics for Constraint Logic Programming oa.upm.es. Checked 19 October 2026.
  3. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy arxiv.org. Checked 19 October 2026.
  4. jsCoq: Towards Hybrid Theorem Proving Interfaces arxiv.org. Checked 19 October 2026.
  5. PICUBE - 2024 - Rapport annuel d'activité radar.inria.fr. Checked 19 October 2026.
  6. Home - Emilio Jesús Gallego Arias x80.org. Checked 19 October 2026.
  7. Une nouvelle culture de la preuve mathématique : le Lean Paris Meetup à Mines Paris – PSL minesparis.psl.eu. Checked 19 October 2026.