Our research focuses on machine reasoning and artificial general intelligence, with mathematics as our primary test case for abstract thinking capabilities.
AI for Mathematics
We treat mathematics as the next game at which machines would excel, serving as a test case for machine reasoning capabilities.
Key Focus: Building autonomous mathematician working 24/7.
▶ DeepAlgebra - an outline of a program, 2016▶ Mathematics in the Age of Large Language Models, 2025
▶ Open Mathematical Problems as an AI Reasoning Benchmark, 2026
▶ UlamAI Prover: An Open-Source Lean 4 Theorem Prover and Formalizer, 2026
▶ Lean for Science Formalization, 2026
▶ ErdosBench: A Research-Mathematics Benchmark, 2026, Github repo, Samples1, Samples2
AI-powered Mathematics
Research level mathematics we have done while testing reasoning capabilities of various LLMs. 16 open Erdos problems claimed (and some formally verified in Lean) with many partial results
Key Focus: Proving research level mathematics with AI. Benchmarking frontier models.
▶ Erdos Problem 1148, full solution (GPT-5.4 Pro), March 2026, formalization in Lean with UlamAI Prover.▶ Erdos Problem 258, full solution (GPT-5.4 Pro), April 2026, formalization in Lean
▶ Erdos Problem 858, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 888, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 514, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 522, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 603, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 610, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 856, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 896, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 953, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 956, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 1092, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 1133, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 1151, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 1090, full solution (GPT-5.5 Pro), April 2026
▶ Erdos Problem 750, full solution (GPT-5.5 Pro), May 2026
Machine Reasoning Theory
Research-level reasoning of large language models.
Key Focus: Mathematical frameworks for human-like reasoning and intelligence.
▶ Research-level Reasoning Trajectories for RLVR, 2026▶ Olympiad-level Math Trajectories, 2026
▶ RAVE and QeRAVE: Router-Aware Virtual Experts for Efficient Mixture-of-Experts LLM Compression, 2026