Joshua Ong

PhD Student @ Imperial College London.

prof_pic.jpg

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

Oct 21, 2026 We are proud to announce that Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation has been awarded the Best Paper Award at the EMNLP MathNLP Workshop πŸŽ‰
Oct 21, 2026 AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language has been accepted at ICSE 2026.
Oct 10, 2026 I will be attending EMNLP 2026 in Budapest, presenting Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean FormalisationπŸ”₯. Feel free to reach out if you’d like to meet or discuss interesting topics!
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πŸ”₯