Selected research
Research systems as well as individual results.
The Ulam atlas is now one of the main things I am building: a reusable map of open-problem difficulty for research selection, evaluation, and downstream tools. The papers below retain the wider portfolio across optimization, graph theory, combinatorics, physics, and model evaluation.
Flagship data and evaluation program
Ulam Open Problem Difficulty Atlas
The atlas replaces a single ambiguous difficulty score with an auditable Open Problem Difficulty Profile. Each record explains not just how difficult a problem appears, but what kind of difficulty it contains, what a human-and-AI workflow could realistically attempt, and how expensive a claimed result would be to verify or formalize.
8,785total problem records
3,359AIM Workshop additions
5,426earlier records preserved exactly
0 / 0errors / warnings in the published validation
What changed in v1.5
A drop-in, append-only expansion.
The 3,359 AIM records were appended under new numeric IDs while the previous 5,426 profiles remained deeply equal to the prior release. Schema, field order, rule version, and problem-ID join semantics stayed stable, so consumers can adopt the new payload without a database migration.
What the expansion reveals
A different problem profile, not simply harder problems.
The AIM additions are only +0.060 higher in mean intrinsic difficulty on a 0–10 scale, but are more specialized, broader, and somewhat harder to formalize and verify. 95.59% fall in the T3 “Serious Project” tier. Their higher tractability is partly a consequence of partial-progress statuses, not evidence of a higher full-solution probability.
What an OPDP measures
Intrinsic difficulty
Conceptual gap, route gap, technical depth, known barriers, and search scale describe why the mathematics itself is difficult.
AI-relative difficulty
A dated protocol estimates where an AI research workflow is likely to struggle, with intervals, confidence, predictors, and fit labels.
Human attention
Specialist-hours and exposure estimates distinguish a deep but well-traveled problem from one that is difficult partly because it is neglected.
Scoped tractability
A probability band estimates meaningful partial progress in 100 combined expert-plus-AI hours; it is not a full-solution probability.
Verification burden
The atlas separates finding a candidate result from the work required to check whether it is actually correct.
Formalization burden
A separate axis estimates how difficult the result would be to encode in a proof assistant or comparably rigid formal system.
Prerequisites and breadth
Depth of background and the number of mathematical areas involved help match projects to the right researchers and tools.
Tool leverage
The profile records whether computation, search, formal methods, retrieval, or other tools are likely to create useful leverage.
Reproducibility
The release includes compressed machine-readable JSON, a seven-sheet workbook, formula audit, rationales, statements, QA queue, methodology, distribution comparison, visual brief, checksums, and citation metadata. Every problem carries public explanations, provenance, confidence, and QA flags.
Limits kept visible
This is a provisional editorial first pass, not expert certification. Open status was not literature-checked for every record; AI difficulty is protocol-dated rather than based on per-problem agent runs; human-hour estimates are priors; and tractability means scoped partial progress in 100 combined expert-plus-AI hours.
The separate CFSD-1000 companion covers only the frozen original 5,426 records. Its 0–1000 values are ordinal editorial estimates, not probabilities, empirical benchmark results, or proof attempts.
Algebraic optimization
Faster matrix multiplication, convolution, and integer arithmetic
The 16 x 16 construction lowers the known variable-multiplication count from 2212 to 2208 and, more importantly, supplies a generalizable search-and-composition method for finding related improvements. The accompanying 5-point cyclic-convolution work reduces the bilinear count from eight to seven over the real field, while the parity-aware multiplication paper studies how trailing-zero structure can eliminate wasted work and shorten carry propagation.
Why it mattersThese papers address arithmetic primitives that recur throughout numerical computing. The practical question is whether the algebra can be translated into stable kernels, compiler transformations, or specialized hardware paths; the research establishes concrete starting points for that engineering work and demonstrates an ability to move from abstract structure to implementation-level constraints.
New graph-theoretic structure
Clique-cluster embeddings and graph encoding
The clique-cluster program encodes multigraphs, weighted graphs, and line structures inside ordinary graph theory by replacing richer relations with controlled clique structure. Follow-up papers develop canonical embeddings into the Rado graph, transfer structural results, correct an overextended weighted-Turan claim, and enumerate the minimum clique sizes needed for faithful coding.
Why it mattersMany operational systems contain order, multiplicity, capacity, or line-like structure that a simple edge does not preserve. A rigorous encoding lets existing graph algorithms and homogeneous-structure theory act on richer systems, opening possible applications in routing, information flow, scheduling, and network comparison while keeping the representation mathematically inspectable.
Combinatorial geometry
New lower bounds for even Kobon numbers
This paper proves an extension principle connecting an odd-line Kobon configuration to the next even case, then combines it with recent optimal constructions to establish new lower bounds for 26, 28, 30, and 32 lines. The derivation was also formalized in Lean 4, providing a machine-checked account of the argument rather than relying only on a diagram or computational search.
Why it mattersThe result shows a useful pattern in my work: isolate a reusable structural step instead of optimizing one isolated instance. That turns a collection of known configurations into a mechanism for generating further bounds and makes future improvements easier to propagate.
Formalized mathematics
No-three-in-line structure and proof techniques
The no-three-in-line work develops a bounded-intersection theorem for quadratic constructions, a modular-lifting framework, and a degree characterization explaining why quadratics occupy a special position. A companion paper systematizes proof techniques across no-three-in-line, the Happy Ending theorem, Erdos-Szekeres, and Ramsey theory, with the central arguments formalized from scratch in Lean 4.
Why it mattersThis is not only a collection of statements. It demonstrates the ability to move between experimentation, finite-field algebra, geometric intuition, and formal verification, which is precisely the combination needed when AI-generated mathematics must become trustworthy enough for expert use.
Bountied open problem
C-finite subsequences of Beatty sequences
This work resolves Clark Kimberling's Special Numbers problem 23 by characterizing when a Beatty sequence contains a homogeneous linearly recurrent subsequence. It connects recurrence, density, category, and transcendence in a form that answers a concrete longstanding question rather than merely reporting computational evidence.
Why it mattersPublicly specified problems are valuable tests of research discipline: the target and success criterion exist before the work begins. Solving one demonstrates that the workflow can navigate unfamiliar literature, formulate the right theorem, and produce an answer that is meaningful outside its own project context.
Open-problem mathematics
Erdos Problem 897: counterexample and explanatory companion
The core paper gives an additive counterexample answering both questions in Erdos Problem 897 negatively. I then wrote a complementary paper that examines the function on small integers, visualizes its envelope, and connects that intuition to the formal proof, making an unfamiliar construction easier to audit and discuss.
Why it mattersA research result creates more value when other people can interrogate it. Pairing a concise proof with computational and visual explanation shows that I can bridge model-generated discovery and human mathematical understanding, including when the result receives skeptical expert attention.
Planetary science
Automated asteroid shape reconstruction
A sequence of papers develops an automated light-curve inversion pipeline spanning dense observations, sparse survey data, convex initialization, non-convex genetic optimization, and self-shadowing ray tracing. One application produced 22 new near-Earth asteroid shape models; the synthesis paper then defined confidence tiers for extracting useful constraints across different levels of data availability.
Why it mattersThis work demonstrates adaptation beyond pure mathematics. The pipeline turns heterogeneous archival observations into physical models at a scale that manual analysis cannot match, with relevance to population science, mission planning, and planetary defense as new survey facilities increase the data volume.
Symbolic physics
PHYSMDT equation discovery
PHYSMDT reframes symbolic regression as iterative masked-token denoising in a 71.6M-parameter model. Its architecture incorporates permutation-invariant observation encoding, expression-tree position, dimensional-consistency bias, and rapid per-problem adaptation; on held-out equations it recovered the magnetic Lorentz force law without having seen that equation during training.
Why it mattersEquation discovery is a demanding test of whether a model can recover compact physical structure from numerical observations. The project illustrates how domain knowledge can be built into an architecture instead of asking a general model to infer every constraint from data alone.
Multimodal evaluation
SpatialBench
As a critical contributor to SpatialBench, I worked on an evaluation framework that decomposes spatial cognition into five levels and 15 tasks, from perception through symbolic reasoning, causal inference, and planning. The benchmark was designed to reveal where apparently strong multimodal systems still rely on surface detail instead of coherent spatial abstraction.
Why it mattersSpatial competence is central to robotics, interfaces, scientific diagrams, and any model expected to act in the physical world. A hierarchical benchmark gives teams a diagnostic map of capability rather than one aggregate score, making failures easier to locate and product improvements easier to target.
Research-level evaluation
Mathematical model evaluation with Ulam and Putnam 86
My evaluation work includes collaboration around Ulam's research-mathematics data and ErdosBench, responsibility for testing the 86th Putnam exam, and the creation of an Open Problem Difficulty Profile for 8,785 UnsolvedMath records. Each profile combines intrinsic and AI-relative difficulty with human attention, scoped tractability, verification, formalization, prerequisites, breadth, tool leverage, uncertainty, provenance, QA flags, and public rationales.
Why it mattersThe atlas is a research-selection and routing system, not a leaderboard. It helps labs and mathematicians choose problems by the kind of difficulty they are equipped to handle, while keeping the assumptions visible enough to challenge, revise, and integrate into downstream tools.