Meet the team
Mathematicians, quants, and engineers building the verification layer for AI agents.
Founders
Cristopher Salvi
Tenured professor of mathematics and AI at Imperial. Cris' research lies at the intersection of stochastic analysis and deep learning. He has made major contributions to generative diffusion models and post-transformer architectures for sequence modelling.
Robert Smith
Former Managing Director and Global Head of Quantitative Research in credit markets at Citi with over 20 years of experience in quantitative financial modelling. Rob built and led global teams integrating AI into advanced trading and risk infrastructure.
Research
Massimiliano Gubinelli
Wallis Professor of mathematics at Oxford. A leading figure in stochastic analysis, Max has made transformative contributions to rough path theory, singular SPDEs, and constructive quantum field theory.
Maud Lemercier
Previously a postdoc at Oxford, Maud made significant contributions in high-dimensional statistics and probabilistic machine learning, with a focus on kernel methods and signature-based models for sequential data.
Tom Klose
A former postdoc at Warwick and Marie Curie Fellow at Oxford, Tom has made contributions at the interface of rough path theory, stochastic PDEs, and mathematical physics, with a focus on singular stochastic dynamics.
Nikolas Tapia
A postdoc at WIAS and Humboldt University, Berlin, Nikolas works across stochastic analysis, rough paths, and signatures, with substantial Lean expertise and contributions to Mathlib.
David Ledvinka
As a postdoc in Kevin Buzzard's group at Imperial, David has made many contributions to the development of analysis and probability theory in Lean.
Justus Springer
A postdoc in Kevin Buzzard's group at Imperial, Justus has contributed extensively to the formalisation of algebraic geometry in Lean, with a focus on computational methods.
Archibald Browne
A PhD student in Kevin Buzzard and Cris Salvi's group at Imperial, Archie has a background in pure mathematics and formal verification.
Eugene Lee
A postgraduate student in Mathematics and Finance at Imperial, Eugene experiments with, optimises, and writes about agentic systems.
Engineering
Krzysztof Kroczak
Krzysztof brings deep software engineering experience in .NET/C# and Azure to shipping AI at scale, working on the platform layer that bridges research and real-world usability.
Juanjo Madrigal
A mathematician with over eight years of experience in functional programming, type theory, and formal verification. Juanjo builds the verification layer behind formalisation blueprints.
Hetvi Bhatt
A software engineer with experience in .NET/C# and Azure, Hetvi is building out the data and API infrastructure that powers blueprint formalisation.
Arav Bhattacharyya
Arav specialises in autoformalisation and Lean metaprogramming. At Logos he builds the tooling that lets agents interact with the Lean compiler.
Francesco Chotuck
An incoming PhD student in pure mathematics at Cambridge, Francesco works on the formalisation of mathematics in Lean.
Hannah Gazet
A software engineer at Logos working in .NET/C# and Azure, Hannah builds the platform that turns research into shippable, real-world AI products.
Alwin Paul
A software engineer experienced in frontend development and scalable platforms, Alwin focuses on intuitive user experiences and reliable, high-quality products.
Jide Oyelayo
A software engineer with experience in .NET/C# backend development and search infrastructure, Jide works on the systems that power search and information retrieval across the platform.
Advisors
Kevin Buzzard
Full professor of pure mathematics at Imperial and the world's leading expert in formal mathematics. Kevin is leading the formalisation of Fermat's Last Theorem, the most technically demanding project in mathematical formalisation to date.
Aitor Muguruza
Chief AI Officer at a systematic hedge fund, with a PhD in AI for financial modelling. Aitor was Risk Magazine's 2020 Rising Star award winner for his work on Deep Learning Volatility.