Joshua Ong
PhD Student @ Imperial College London.
I am a first-year PhD student at Imperial College London, fortunate to be advised by Eleonora Giunchiglia, Shay Cohen and Wenda Li, and am currently a visiting researcher at the Institute of Foundation Models, part of the Mohamed bin Zayed University of Artificial Intelligence (MBZUAI). Prior to joining Imperial College London, I was a visiting researcher at the University of Edinburgh, where I also obtained my BSc in Mathematics and Statistics.
My research focuses on Large Language Model (LLM) Reasoning and theorem proving, with a particular interest in understanding and improving the mathematical reasoning capabilities of LLMs. Currently, my interests lie in generating verifiable synthetic data for LLMs [1], and training reasoning models for both formal and informal mathematics [2]. I am also part of the AI for Math Grant, where our main focus lies in advancing theorem proving autoformalisation within LLMs.
PhD and Masterโs applications and stepping into research can be overwhelming. As such, Iโd love to dedicate time to helping anyone who wants to chat or seek advice about the process. Feel free to reach out if youโd like to discuss research, explore collaboration opportunities, or just talk through your questions, Iโm more than happy to help!
I am actively looking for internship opportunities for 2027. Feel free to reach out to me if there are any interesting or suitable positions!
news
| Sep 25, 2026 | SCOPE: Self-Play via Co-Evolving Policies for Open-Ended Tasks has been accepted at NeurIPS 2026. |
|---|---|
| Sep 11, 2026 | ๐๐๐ We are pleased to release Magenta, an end-to-end formal-informal self-correction pipeline that achieves 100% mathematical benchmarks, marking the first time a fully open-source model has achieved a perfect score. In addition, when using a 7B model for informal reasoning, the pipeline achieved a perfect score on IMO 2026, making it the smallest model to date to do so. For more details, please see our recent work, Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification๐ฅ. |
| Jun 12, 2026 | ๐๐๐ We are pleased to release Pythagoras-Prover, a family of theorem-proving models (4B and 32B). It includes the smallest model to date for theorem proving (4B), as well as the first diffusion-based model capable of theorem proving. For more details, please see our recent work, Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation๐ฅ. |
| Jun 01, 2026 | I will be attending ICML 2026 in Seoul ๐ฐ๐ท. Feel free to reach out if youโd like to meet or discuss interesting topics! |
| May 01, 2026 | Can I Have Your Order? Monte-Carlo Tree Search for Slot Filling Ordering in Diffusion Language Models has been accepted at ICML 2026. |
| Apr 07, 2026 | PiCSAR: Probabilistic Confidence Selection And Ranking for Reasoning Chains has been accepted at ACL 2026 (Findings). |
| Feb 16, 2026 | Do check out our recent work on Can I Have Your Order? Monte-Carlo Tree Search for Slot Filling Ordering in Diffusion Language Models๐ฅ |
| Feb 01, 2026 | I am excited to announce that I will be joining MBZUAI as a visiting student, working on Theorem Proving with LLMs. Feel free to reach out if you are interested in discussing potential collaborations! |
| Jan 26, 2026 | Neural Theorem Proving For Verification Conditions: A Real-World Benchmark has been accepted at ICLR 2026 (Poster). |
| Oct 25, 2025 | I will be going to EMNLP 2025 in Suzhou, China. Feel free to reach out if youโd like to meet or discuss interesting topics! |