Mahdi Bu Ali

About

Mahdi Bu Ali completed his MSc in Computer Science at KAUST in 2025 under the supervision of Robert Hoehndorf. His research lay at the intersection of formal mathematics, automated theorem proving, and large language models.

His thesis, Automated Theorem Proving with Large Language Models in Lean: An Exploration of Specialized In-Context Learning and General-Purpose Hierarchical Architectures, addresses the long-standing goal of automating mathematical reasoning in interactive theorem provers such as Lean. Automated theorem proving is constrained both by the cost of exploring vast proof search spaces and by the gap between informal mathematical intuition and the rigorous, machine-checkable proof steps that systems like Lean require. Building on recent work showing that transformer-based language models can generate complete proof steps end-to-end, the thesis explores two complementary strategies for closing the informal-to-formal gap: specialised in-context learning regimes that exploit the structure of Lean tactic proofs, and more general-purpose hierarchical architectures that decompose proof search into higher-level planning and lower-level tactic generation.

The work contributes to the group's emerging research line on neuro-symbolic AI and on the use of large language models for structured, verifiable reasoning over formal artefacts. It complements ongoing research on combining symbolic knowledge representation with neural methods, and provides an empirical evaluation of how far current LLMs can be pushed on formal proof tasks when paired with appropriately engineered context and architectural scaffolding.