Researchers in mechanistic interpretability, harness design and formal verification.

Currently in MATS 9.1 with Simplex, after a Physics PhD at the University of Amsterdam and a MARS 3.0 with Geodesic Research. Likes to work on mechanistic interpretability, even though it is damn hard.

Currently an Iliad fellow, after a postdoc at EPFL and a PhD in string theory at University of Bonn. Likes mechanistic interpretability, formal verification, and believes that AI safety should eventually mostly run itself.

Trained in signal processing, statistical machine learning and theoretical neuroscience, with a PhD thesis that used RNNs as model organisms for cortical circuits. Has been moving into AI safety and alignment since last year.

A theoretical physicist with a PhD from Oxford and a postdoc at the Technion, with a background in holography, black holes and hydrodynamics. His machine learning interests are optimization, generalization and interpretability.

A mathematician who recently completed a PhD at the University of South Carolina, working on algebraic and arithmetic geometry, commutative algebra and representation theory. Lately works on formalization and autoformalization of mathematics, and on what goes wrong when agents do the formalizing.

A software engineer working on context infrastructure for LLMs. Built ContextGraph, which lays an LLM session out as a graph of context atoms on a canvas to keep plausible-looking but wrong output in check, and that problem is what pulled him toward alignment research.

A mathematics student working on formal verification and autoformalization with Lean, including the LeanAide project, with a background in mathematical logic and foundations. In machine learning, interested in interpretability and reinforcement learning.

An AI/ML engineer based in Calgary who builds evaluation infrastructure for LLMs and agents, and maintains a few open source libraries on the side. Here to make the autoresearch runs easier to audit, and to learn from the math side of the team.

An independent researcher in type theoretic formalization of AI and complex systems, with a triple MSc in Mathematical Modelling in Engineering. Likes emergent properties of ANNs and interpretability.

An independent researcher with an MSc in Mathematics, recently working on formalized mathematics, automated theorem proving, and AI-assisted mathematical reasoning. Likes to spend his free time thinking about mirror symmetry.

Studying applied mathematics at UC Berkeley, with an interest in the intersection of mathematics and machine learning. Likes exploring new areas of mathematics and learning from others through collaboration.