Blog

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.