Nikol Savova
Mathematician. About to begin the final year of the integrated master’s at Oxford, where I also read my undergraduate degree. Before that, olympiad mathematics at the Sofia High School of Mathematics.
mathematics
Logic, set theory, Galois theory, algebraic number theory, graph theory, probability, and the history of mathematics, including a mini-dissertation on Fermat’s Last Theorem and the attempts that preceded the proof.
research
At eighteen, research assistant to Dr. Igor Balla in spectral graph theory, generalising the Alon–Boppana theorem from regular to arbitrary graphs, replacing the adjacency matrix with the Laplacian, taking Fiedler’s algebraic connectivity λ2 as the object of interest, and looking for lower bounds on the spectral gap that remain meaningful in the dense regime, where the classical bound degenerates. Connected to the positive discrepancy disc+(G).
papers
Four so far, grown out of Proof Hunter: an exhaustive verification of Brenti’s conjecture on log-concavity of Bruhat intervals, a counterexample settling two open problems in Bregman–Chebyshev theory, and partial progress on two ErdÅ‘s problems. full list →
philosophy
The parallel track. I wrote philosophical essays in Bulgarian and hosted philosophical gatherings in Sofia for several years. Continental philosophy, mostly. And the hybrid territory between mathematics and philosophy, what logic and set theory mean when read philosophically.
detours
- Since August 2026, generalist expert for Mercor, evaluating AI model outputs for AI research partners.
- Attended a run of selective applied-rationality programs (WARP 2022, ESPR 2022, Future Forum 2022), then returned as junior counsellor at ESPR 2023, and again at PAIR 2026 this August.
- Head of quantitative research at Bloomsbury Technology, a pre-seed art-valuation startup (Jan–Apr 2026), until its focus changed.
- Taught olympiad mathematics, 2022–2024.
- Emergent Ventures Fellow (Mercatus Center, 2023). Pitched Tyler Cowen a continental philosophy podcast. Received a grant for general development instead.
currently
Building Proof Hunter, a pipeline for finding open problems in mathematics that are tractable, verifiable, and genuinely unsolved, then attempting them with AI. It has turned into an active proof campaign, with four papers so far, each shipped with the code and certificates that check its claims, since I’m not the one qualified to vouch for them otherwise. Learning Lean, since cracking open problems will require it.
Since September 2026, Founding AI Alignment Researcher at IVORI Lab, working on a foundation social world model for decision-making under uncertainty, combining normative, philosophical, biological, mathematical and computational perspectives.
Hacking learning how to learn. Headed toward quant finance and game theory.
conjectures
- AGI is not coming. The people building it haven’t changed my mind. the argument →
- Formalisation will change what it feels like to do mathematics before it changes what mathematics gets done.
- As proving gets cheaper, the scarce skill in mathematics becomes knowing which problems are worth attempting.
- Hard open problems are calibration instruments. They map where a field’s language breaks.
- Benacerraf was right, and Lean is the evidence. Mathematical objects are positions in structures.
- There are rational reasons to make irrational decisions from time to time.