alejandrozarzuelo.com
Mathematical researcher building exact constructions, formal proofs, and research systems for the AI frontier.
I choose difficult problems, develop the mathematics with AI, and turn the results into proofs, datasets, and public tools. My recent work spans improved matrix multiplication, Kobon triangle constructions, Polyhedra in Polyhedra, and clique-cluster graph theory. I built the 102,819-record Ulam Open Problem Difficulty Atlas, published an assessment of 722 AI mathematics manuscripts, and helped organize and review research for OpenMath. I also developed the methodology for SpatialBench, a benchmark that guarantees visual intelligence, and created MeloText-ID, measuring capabilities before large recorded model-score jumps.
Recent research milestones
My work covers the whole research process: choosing a worthwhile question, finding a construction, checking the claim, and building the tools that let others investigate it. The latest projects bring together original mathematics, formal evidence, and real use in research selection and scientific events.
My recent work connects algebraic constructions, geometric search, exact certificates, and Lean verification. I have developed a general matrix-composition framework, expanded my Kobon triangle constructions, and built a public packing research platform extending from Platonic solids into higher dimensions. I choose the mathematical direction, develop the argument with AI, and make the resulting claims inspectable.
Explore the signature researchI helped design the scientific framework for OpenMath, curated its research problems, co-hosted the September 27 formal-verification hack at Harvard Innovation Labs, gave a lecture, and carried out detailed mathematical review of submissions. My Ulam Difficulty Atlas supplied the basis for the six competition problems, connecting research judgment to an event people could actually work on.
Read the official event pageI expanded the Ulam Open Problem Difficulty Atlas to combine 15,458 statement-bearing records, 87,105 MathDB excerpts, and 256 source-normalized ProofAtlas entries. Provenance and confidence travel with the data, making it a practical research-navigation system.
Explore the current atlasI published a 254-page assessment of a frozen 722-manuscript snapshot of the OpenAI mathematics release, covering 372 result families and 17 disciplines. The report compares theorem scope and partial progress against the atlas, with a readable overview and machine-readable rationales.
Read the assessment overviewMy merged contribution to the community integer-multiplication project combines formal proofs, Gaussian-parity structure, and exact precision accounting. It includes 99 new Lean theorems within a 168-theorem audit, alongside 10,732,176 exact coefficient checks.
Read the merged contributionI select problems, design evaluations, direct AI-assisted investigation, and turn promising output into explicit arguments, reproducible artifacts, and public research tools.
Signature researchMy recent work includes OpenMath mathematical submission review, jury service at the seventh HackNation Global AI Hackathon, and judging the September 19 VoiceAI hackathon at AGI House.
Events and trajectoryIn San Francisco, I have regularly attended and participated in Frontier Research Club events, joining technical talks, extended discussions, and peer critique across AI and science.
Frontier Research ClubI presented at the first iteration and became a collaborator and organizer of recurring events. That work has grown into problem selection, scientific rules, lectures, and formal-verification events with the wider community.
RSI House eventsBenchmarks
I look for important capabilities and research directions before they become obvious. SpatialBench and MeloText-ID preserve measurements from before large capability jumps. The expanded Ulam atlas, the OpenAI mathematics assessment, and CostFloor turn that same research judgment into tools other people can examine and use.
Featured benchmark · measured before the capability jump
I collaborated with Geby Jaff (@spicey_lemonade) on this public 50-problem benchmark for 2D path tracing and 3D mental rotation. I developed its probability-equivalence scoring method and the structural mathematical framing for the two task families, building a measurement for a capability frontier that had substantial room to move.
The published leaderboard records 67.07% for GPT-6 Astra without tools and 91.78% with Code Interpreter, compared with earlier listed scores of 2.95–13.5%. Creating the measurement before that jump was a directional forecast about visual capabilities, with a frozen public artifact against which that judgment can be assessed. Its 50 questions measure these particular tasks.
Expanded research infrastructure · OPDP v1.8
A research map covering 102,819 records, with separate dimensions for intrinsic and AI-relative difficulty, tractability, verification, formalization, prerequisites, and tool use. The atlas now combines the original full-statement cohorts with MathDB excerpts and normalized ProofAtlas intake.
The total includes 15,458 statement-bearing records, 87,105 excerpt-only MathDB records, and 256 source-normalized ProofAtlas records. The latter two cohorts retain C0 provisional confidence. Source-linked estimates support research selection, and the official September 27 Sundai event used the atlas as the basis for its six problems.
October 2026 · independent research assessment
I assessed a frozen 722-manuscript snapshot of the OpenAI mathematics release against the atlas, organizing 372 result families across 17 disciplines. A 254-page report, executive brief, and structured data explain how each manuscript relates to a research target and where its contribution sits.
The assessment distinguishes related targets, partial or special cases, lexical candidates, and same-target scope matches. The 59 same-target matches are scope classifications, not certified solutions. This is my independent assessment, with a separate overlay preserving the canonical atlas.
Audited benchmark · MeloText-ID v0.2.0
A benchmark I created for recognizing familiar melodies from sparse symbolic notes, across transposition and with or without explicit durations. Twenty models choose among 25 titles in four matched conditions, with repeated balanced trials, exact grading, and frozen task commitments.
The public audit retains 20,000 scored decisions across two sealed runs. GPT-6 Astra leads at 71.38% against 4% chance, 30.02 points above the pilot's 41.36% best. Public protocol, aggregate results, and audit artifacts make that cross-representation capability jump inspectable.
Applied model · automation and physical costs
An auditable scenario engine for exploring product costs when labor and capital are recursively replaced with physical inputs under automation. It separates energy, materials, scarcity, taxes, and margins, with editable assumptions and visible replacement steps.
The prototype includes six reconciled fixtures and low/base/high scenarios with recursion controls. Its purpose is to expose the assumptions behind post-automation cost claims and make them editable, rather than hide them inside a single forecast.
Continuing programs
Turning the atlas into curated research tasks, formalization requirements, evaluation criteria, and reproducible submission reviews. This includes separating a correct partial result from the larger open problem it contributes to.
Developing inspectable measurements of capabilities that were weak when the tasks were created, so later progress can be compared against frozen protocols, scoring, and evidence. SpatialBench and MeloText-ID preserve that record across visual and musical representations.
Signature work
Four programs show how I work: exact algebra, combinatorial geometry, certified packing, and graph encoding. Each has a public path from the mathematical claim to its sources, construction, or proof evidence.
Certified algebraic construction
I started with an order-16 construction using 2,208 scheduled variable multiplications, then developed a general synthesis framework connecting matrix-valued identities to commutative scalar computations. The October manuscript adds certified block and instruction-program composition, plus a denominator-cleared integer implementation whose outputs are divided exactly by eight. The concrete 16 x 16 result is one instance of the broader construction, with its algebraic assumptions and reusable interfaces made explicit.
Infinite families and geometric bounds
I expanded the Kobon program from finite examples into explicit real-line construction families, an all-order lower-bound refinement, and a deficit-dependent successor rule. The October release includes a 15-page article and an 88-page companion with detailed arguments, coordinate catalogues, and a claim-to-source map. The work combines geometric construction, structural incidence bounds, exact finite certificates, and formal proofs while retaining the credit of earlier numerical seeds and construction methods.
Autonomous search, exact geometry, formal proofs
I generalized a soft-to-rigid cube-packing search into a research platform for placing polyhedra inside polyhedra, pairing numerical exploration with exact feasibility certificates and an interactive public catalogue. Two papers study the method and the structure of 351 frozen constructions. The program has since expanded across 140 frozen shape families in three through six dimensions, with 532 selected packing witnesses verified in Lean at their recorded placements and scales.
Recovering richer structure from simple graphs
I developed clique-cluster encodings for graph multiplicities and line structure, then made the decoding and enumeration claims more precise through formal proofs and exhaustive checks. The current work separates strict-dominance cluster identification from an alternative unused-port decoder that recovers the unmarked cluster family and its multiplicities under a capacity condition. Six OEIS sequences count labeled graphs and bounded-multiplicity graphs by clique number, with every retained term through eight vertices independently reproduced.
Where this matters
I contribute across research direction, formal reasoning, implementation, and evaluation, especially where a good mathematical model changes what a team can build or verify.
I bring problem selection, theorem scope, formalization, exact certificates, and research evaluation together. My current direction is to make more scientific reasoning machine-checkable, while preserving the human judgment needed to choose worthwhile questions.
Matrix composition, integer multiplication, precision accounting, and proof-oriented implementation connect my mathematics to compilers, numerical infrastructure, and the arithmetic behind modern compute.
I can turn an open-ended program into curated tasks, scientific rules, evaluation criteria, and evidence-backed reviews, as demonstrated by OpenMath and the atlas's manuscript assessment.
Packing, optical simulation, and line-structured graph models let me move between abstract mathematics, geometric computation, and physical or operational systems.
Trajectory
The through-line is simple: select meaningful problems, use frontier models where they are strongest, pressure-test them where they fail, and convert raw output into artifacts that survive review.
October 2026
Built Polyhedra in Polyhedra, released two papers and a frozen 351-construction archive, and expanded the program into a 140-family formal catalogue with 532 selected Lean-verified witnesses. The public viewer connects constructions, source attribution, and proof evidence.
September–October 2026
Helped design the research and evaluation framework, selected problems, co-hosted the September 27 Sundai formal-verification event at Harvard Innovation Labs, gave a lecture, and reviewed mathematical submissions. The official event page credits my atlas as the basis of the competition.
October 2026
Served on the jury and evaluated submitted AI projects for creativity, communication, and technical depth. The October 4 judging session and the organizer-issued certificate document the completed contribution.
September 2026
Judged the September 19 VoiceAI hackathon at AGI House, an event supported by SambaNova, General Compute, Infinity, and Hume. This added applied product and technical evaluation to my mathematical judging work.
2026
Expanded the Ulam Difficulty Atlas to 102,819 source-linked records, developed a 100-sprint mathematics research agenda, and assessed a frozen snapshot of 722 OpenAI mathematics manuscripts across 17 disciplines. SpatialBench and MeloText-ID preserve the earlier measurement of capabilities before large model-score jumps.
2026
Developed the general matrix-composition construction, expanded Kobon triangle families, strengthened clique-cluster decoding and sequence checks, and contributed exact arithmetic and formal verification upstream. I combine mathematical direction with AI-assisted development and reproducible evidence.
2025–2026
I was the lead scientist at Archivara, where my work helped create the technical story behind its reported YC S26 path and reported $25M valuation. I selected questions and directed AI-assisted mathematics and physics research, including early open-problem investigations and work presented for public mathematical scrutiny.
2025–2026
Directed prompting, scaffolding, verification, and exposition for the Erdős 897 counterexample workflow, discussed publicly by Terence Tao and others. The record includes the later priority clarification as an independent rediscovery. I also worked on bountied problems and the limits of AI-generated mathematical arguments.
Community
A fellow of both communities, I have regularly participated in San Francisco research events. After presenting at the first RSI iteration, I became a collaborator and organizer, extending that work into scientific problem selection, talks, and verification-focused events.
2024
Worked in an INRIA research environment, developing the habits behind my later optimization, mathematical modeling, and AI-assisted research.
Education
Trained across physics and mathematics, with thesis work on optimization in line-structured networks and optical light recycling. My public repositories retain the mathematical models and optical simulation work.
What I do
Selected research
I build infrastructure for choosing research questions as well as individual mathematical results. The current portfolio connects exact arithmetic, geometry, formal proofs, scientific review, multimodal evaluation, and physical modeling.
Research infrastructure · OPDP v1.8
I designed the Open Problem Difficulty Profile to explain what makes a mathematical target difficult, what progress a human-and-AI workflow could attempt, and what it would cost to verify or formalize a result. The current archive contains 102,819 records across three distinct intake blocks, each retaining its source and confidence level.
What changed in v1.8
The original cohort combines UnsolvedMath, AIM, and Oberwolfach records. Later releases add MathDB excerpts and distinct ProofAtlas targets, with reversible identifiers and checks preserving the frozen earlier prefix. The new intake records retain C0 provisional confidence and explicit statement limits.
From the atlas to an assessment
My October assessment maps the frozen OpenAI mathematics release, 722 manuscripts and 372 result families in 17 disciplines, against the atlas. The 254-page report and structured rationales distinguish full-target scope from related, partial, and special-case results. The assessment is a separate overlay.
What an OPDP measures
Conceptual gap, route gap, technical depth, known barriers, and search scale describe why the mathematics itself is difficult.
A dated protocol estimates where an AI research workflow is likely to struggle, with intervals, confidence, predictors, and fit labels.
Specialist-hours and exposure estimates distinguish a deep but well-traveled problem from one that is difficult partly because it is neglected.
A probability band estimates meaningful partial progress in 100 combined expert-plus-AI hours; it is not a full-solution probability.
The atlas separates finding a candidate result from the work required to check whether it is actually correct.
A separate axis estimates how difficult the result would be to encode in a proof assistant or comparably rigid formal system.
Depth of background and the number of mathematical areas involved help match projects to the right researchers and tools.
The profile records whether computation, search, formal methods, retrieval, or other tools are likely to create useful leverage.
Used in a real research setting
The official Sundai Hack 142 program credits the atlas as the basis for its six competition problems. Related public work includes a 100-sprint research agenda, a formal statement corpus, and scoped computational and formal results.
How to read the data
Difficulty and tractability are source-linked editorial estimates. Record counts include excerpts and provisional normalizations, with no blanket verification of current open status. The current v1.8 data are JSON; the retained workbook covers the earlier v1.6 cohort.
Wider portfolio
Algebraic optimization
The revised matrix program gives reusable interfaces for combining bilinear matrix-valued outer identities with commutative scalar leaves. Its order-16 instance schedules 2,208 products, and a denominator-cleared realization keeps intermediates integral with exact output division. The general theorems state the component-validity assumptions that permit larger compositions.
This work makes algebraic improvements precise enough to inspect and reuse, with a bridge from mathematical identities to verified arithmetic programs.
Upstream research contribution
My merged upstream PR45 develops Gaussian-parity structure, exact producer integration, and precision accounting, with 168 audited Lean theorems and 10,732,176 exact coefficient checks. Later public proposals explore profile-aware compilation and conditional parameter refinements within the community's wider analytic framework.
This is research engineering at the interface between algebra, implementation, and proof. The linked contributions identify my work, their assumptions, and their upstream status.
Combinatorial geometry
The October release develops explicit real-line construction families, a uniform lower-bound refinement, compatible seed iteration, and a deficit-dependent successor rule. A 15-page article and an 88-page companion connect the geometric arguments to finite coordinate certificates and a detailed proof map.
The program advances constructive methods across infinitely many orders while making the relationship between numerical examples, general arguments, and formal evidence visible.
Computational geometry
Polyhedra in Polyhedra combines autonomous search, exact containment and separation checks, an interactive catalogue, and selected Lean witnesses. The original nine-pair dataset has 351 certified constructions; the current frozen formal catalogue extends across 140 families, with 532 selected source-bound witnesses in dimensions three through six.
Explicit geometry and certificates support further work on confinement, configuration space, contact structure, and periodic motifs. The materials-science guide connects these mathematical objects to established research questions.
Graph theory
The current clique-cluster work studies recovery of cluster structure and multiplicities under explicit decoding conditions. Six OEIS sequences are reproduced through eight vertices, including a complete eight-vertex graph census, and Lean developments verify distribution identities, row totals, and decoding interfaces.
A graph representation is useful when the richer structure it encodes can be recovered. This program turns that requirement into explicit hypotheses, algorithms, enumerations, and proofs.
Reproduction and refinement
I reproduced Jensen Kohlmeyer and Liam Kruer's original construction in a pinned Lean environment and developed an implementation and least-saturation refinement. The supplement includes ten audited declarations, 4,407 finite extension checks, and a worked example reducing the saturation length from 16 to 11 for the specified rule.
This work shows how I turn an existing argument into an explicit, tested artifact, identify a scoped improvement, and preserve the original mathematical credit.
Research infrastructure
I built and maintained a public review archive linking submitted sources, problem-family profiles, contribution notes, proof evidence, and author-review material. The work includes mathematical triage, correctness and novelty assessment, reproducibility, and careful separation of individual contributions from combined research progress.
Running a serious AI mathematics event requires scientific judgment after the models stop generating. My contribution connects research selection to the detailed work of assessing what a submission actually establishes.
Formalization and research selection
Formalization Lab collects 200 attributed open-problem statements with source provenance and elementary proved controls. A separate 100-sprint agenda spans 16 mathematical fields. The OPDP attempt repository records scoped finite results, exact certificates, and the remaining general problems.
This is a practical route from a large research landscape to an executable project: choose a bounded target, make the statement precise, and define what checkable progress would look like.
Multimodal evaluation
SpatialBench combines 25 path-tracing tasks and 25 mental-rotation tasks with different chance baselines. I developed probability-equivalence scoring and its mathematical framing with Geby Jaff. MeloText-ID asks a related cross-representation question using symbolic melodies, controlled transposition, and duration conditions.
I built these measurements before major recorded score jumps. They reflect an interest in predicting which under-measured capabilities will matter, then preserving evidence that lets the prediction be evaluated later.
Physics and mathematical modeling
My university research connects optical light recycling and ray simulation with optimization models for networks whose line structure matters. These projects supplied a foundation for later geometric computation, clique-cluster modeling, and scientific reasoning work.
The combination of physics and mathematics lets me move from abstract structure to physical constraints and computational models, rather than treating a formal theorem as the whole engineering problem.
Benchmarks and collaborations
My benchmark interests are centered on research behavior: whether models can find obstructions, avoid false solved claims, reason over spatial structure, and generate outputs that humans can verify.
An independent 254-page, source-linked comparison of 722 manuscripts and 372 result families with the frozen atlas.
Ulam / Open Problem Difficulty Atlas102,819 mixed records, with explicit statement-bearing, excerpt-only, and source-normalized cohorts, provenance, and confidence.
MeloText-IDTwenty models, 20,000 scored decisions, and four controlled conditions for familiar-melody recognition from symbolic text.
SpatialBenchFifty public spatial tasks, with the scoring methodology and structural mathematical framing I developed before the large recorded capability jump.
Formalization LabA source-attributed corpus of 200 mathematical problem statements, with elementary proved controls and explicit formalization boundaries.
CostFloorAn interactive model for exploring automation-adjusted physical resource floors through editable assumptions and recursive accounting.
Other things I build
Personal urban-design and mapping prototypes, built from the same interest in structure, computation, and useful visual tools.
A personal urban-design proposal built around a 200-by-200-meter LiDAR and open-data model of Castro and Market, with an interactive 3D plaza and fountain study.
Arrondissements of San FranciscoAn interactive proposal for 15 numbered districts in three rings, combining neighborhood search with area and population comparisons from public geographic data.
Blog
Notes on mathematics, AI capabilities, and the ideas I am working through.
The next chapter
This is where I will share longer pieces, research notes, and reflections on the work behind my projects.
Contact
I welcome conversations about mathematical AI, formal verification, exact arithmetic, geometric computation, research evaluation, and scientific tools. I am also interested in talks, judging, and collaborations that turn an ambitious question into checkable progress.