Ulam is a research lab exploring intelligence through mathematics and turning that work into systems that can be deployed. Our model is publish + ship: advance core research, then apply it where correctness, efficiency, and reliability matter.
We focus on quantization, architecture discovery, verified reasoning, and evaluation science, then translate these results into product tracks in AI assurance, semiconductor verification, and model efficiency engineering.
We pursue research that improves both scientific capability and operating economics under real constraints.
Geometry-guided methods that reduce cost and latency while preserving performance in production settings.
New model structures informed by invariances and representation theory, with emphasis on reliability and control.
Formalization and checker-backed workflows where outputs are auditable instead of assumed correct.
Benchmarks, theorem workflows, and open problem tracks that push model reasoning beyond pattern-matching.
Release gating, regression tracking, and evidence trails for teams shipping agentic systems in production.
Requirement-to-proof workflows that integrate with existing formal toolchains to catch high-impact issues before milestone freeze.
High-signal datasets and benchmark infrastructure for model builders who need harder-to-game evaluation.
Applied optimization programs for organizations where inference cost and latency define product viability.
Discovery (2-3 weeks): define API boundary, select one high-value scope, and lock measurable KPIs.
Pilot (10-12 weeks): deliver working pipeline on one real use case with evidence artifacts and one deployment gate.
Expansion: move to annual platform deployment with governance controls and reusable program templates.
UlamAI Prover is our open-source workflow for turning natural-language mathematics into machine-checkable outputs. This verification discipline now extends into enterprise workflows for AI assurance and high-assurance engineering. See repository.
We released UnsolvedMath, a curated set of 1,146 open mathematical problems designed to evaluate reasoning systems beyond benchmark saturation.
Read full article →