Blog

An arXiv-like public record for AI-generated research, with explicit verification scope, downloadable source, and a foundation for building better reasoning datasets.

Public benchmarks are useful, but they are not release gates. Private evaluations reveal whether a model can reason reliably on the capabilities that matter - and what to train next.

RAVE introduces router-aware virtual experts—a middle path between pruning and merging MoE experts. In an internal SU-01 proof-judging pilot, RAVE-64 led the aggregate leaderboard while using a 50% expert-centroid budget.

We are building a low-contamination math benchmark from synthetic Erdős-style research problems and IMO-like proof problems—testing not just final answers, but rigor, partial progress, and honesty about gaps.

We used GPT-5.4 Pro, Opus 4.6, and GPT-5.2 to attack open problems in mathematics—and one of them is now fully settled, with a machine-checked proof in Lean 4.

We're releasing UlamAI Prover, a truth-first CLI that combines LLM-guided reasoning with Lean 4 verification to produce machine-checked proofs—no hallucinations, no trust required.

We're releasing a research repository that uses LLMs to verify Gaitsgory's proof of the Geometric Langlands Conjecture and transfer its methods to ℓ-adic and p-adic settings—opening a new paradigm for testing AI mathematical reasoning on theory-building, not just problem-solving.

We're releasing UnsolvedMath, a curated collection of 1,146 open mathematical problems designed to benchmark AI reasoning capabilities on problems that humanity hasn't yet solved.

We're building an AI research lab focused on inference economics—methods that make modern language models cheaper, faster, and more reliable in the real world.

Few words about the blog. Welcome to the ULAM blog where we share our thoughts on artificial intelligence, machine learning, and their practical applications in business.

Our articles explore both theoretical aspects of AI research and real-world implementations across various industries.