Triviality
Inspiration
Have you ever lain in bed at night wondering, “Is it possible for a 23-cell shell in a trihexagonal tiling to enclose more than the predicted maximum of 29 cells?”
With 36 hours (-4 for sleep), far too many Red Bulls, and four dedicated idiots, we created a harness and swarm of AI researchers that solved unsolved math problems (including that one).
We wanted to see what happens when you take an exploratory and evolutionary approach to tackling math research. The result is Triviality, a workspace for exploring mathematical problems, coordinating research agents, and inspecting the evidence behind their conclusions with formal proof checkers.
What it does
Triviality combines an interactive mathematical atlas with a workspace for running AI research teams.
Explore the graph, select a problem, read its statement and sources, and send it directly into the research workspace.
Each team has six roles:
- One coordinator develops distinct approaches and assigns research directions.
- Three researchers investigate those approaches in parallel.
- One challenger examines their findings for gaps, unsupported assumptions, and counterexamples.
- One proof writer turns reviewed arguments into formal proof candidates and written explanations.
Researchers share findings through a persistent discovery bank. The challenger’s feedback returns to them for another round. When an approach is refuted or stops making progress, the coordinator can assign a new direction while preserving the record of what failed.
Even AI occasionally needs someone to say, “We tried that already bro.”
Users can choose models for individual roles, configure research limits, and inspect the investigation’s progress, findings, and artifacts.
Results
1. A counterexample to the trihexagonal shell bound
The proposed formula claims that a shell containing S cells can enclose at most
$$ \left\lfloor \frac{s^2+6}{18} \right\rfloor $$
cells.
Our featured counterexample is a connected shell of 23 cells enclosing a connected region of 31 cells.
For a shell of that size, the proposed bound gives
$$ \left\lfloor \frac{23^2+6}{18} \right\rfloor = \left\lfloor \frac{535}{18} \right\rfloor = 29 $$
Two extra cells. A rather significant problem for the formula.
The accompanying Lean 4 / Mathlib certificate checks the finite construction: cell counts, disjointness, connectivity, boundary relationships, and the arithmetic contradiction. We published the mathematical explanation and downloadable Lean source.
2. Finding the optimum on a constrained 5×5 grid
The next problem asks how many cells can be marked on a 5×5 grid while satisfying two restrictions:
- No rectangles: No four marked cells form the corners of a rectangle with horizontal and vertical sides.
- Diagonal limit: Every diagonal in either 45° direction contains at most two marked cells.
The answer is exactly 12.
To prove the upper bound, count pairs of marked columns within each row. No pair can appear in two rows, since that would create a rectangle. Only 10 pairs of columns are available (5 choose 2).
With 13 marks, even the most evenly distributed row counts, (3,3,3,2,2), require
$$ 3\binom{3}{2}+2\binom{2}{2}=11>10, $$
so 13 is impossible—even without the diagonal restriction.
This arrangement achieves 12 and satisfies both restrictions:
● ● ● · ●
· · · ● ●
· ● · ● ·
● · · ● ·
· · ● ● ·
The upper bound and matching construction prove the optimum is exactly 12.
Sometimes mathematical research needs a sophisticated construction. Sometimes it needs counting to eleven and realizing you only had ten.
How we built it
The mathematical workspace
We built the frontend with Next.js, React, TypeScript, and Tailwind CSS.
The atlas uses Three.js and react-force-graph-3d to display mathematical areas, problems, and research relationships. KaTeX renders mathematical notation in problem descriptions and research documents.
The research harness
Our WorkSwarm orchestration layer, built around openJiuwen SwarmFlow, manages the research process.
A Python runtime executes the research branches and routes model requests by role. A Node.js worker receives structured events and persists the investigation.
The three researchers work concurrently within exploration rounds. Findings are shared before the challenger evaluates them, allowing the team to compare approaches and respond to criticism.
Reviewed candidates go to the proof writer. Lean failures return feedback to the research process rather than disappearing behind a generic error.
Memory and literature
MongoDB stores research episodes, discoveries, literature, and graph relationships. Redis queues research jobs independently of the browser.
Literature retrieval uses OpenAlex alongside stored materials. Discoveries retain source references, branch information, and evidence status so users can trace how an argument developed.
Verification
A model saying “proved” does not finish the job.
Generated proof candidates are submitted to Lean. Rejected or unchecked candidates remain distinguishable from successfully checked artifacts.
Additionally, when a model generates the formal statement itself, a human still needs to review whether that statement faithfully represents the original problem.
Huawei OpenSwarm
We used Huawei’s openJiuwen SwarmFlow to coordinate our six-agent research team. Researchers explore different approaches in parallel, share discoveries, and respond to the challenger’s feedback before passing reviewed arguments to the proof writer.
Vultr
We used Vultr to host our mathematical experiment worker and Lean runner. Agents can test conjectures, search for counterexamples with exact arithmetic, and submit formal proof candidates for checking. Experimental results and Lean feedback feed back into the research process to guide the next round.
Challenges we ran into
Making the agents collaborate usefully
Multiple agents can repeat the same idea with slightly different wording. We gave researchers separate approaches and contexts, then added explicit evidence-sharing boundaries and structured challenges.
The goal was to make disagreement productive.
Knowing when to restart
A failed Lean tactic does not necessarily invalidate the mathematical argument. A counterexample can.
Our workflow distinguishes reported refutations, stagnation, and formalization failures so that each produces an appropriate next step.
Keeping evidence and confidence separate
A researcher’s claim, a challenger’s approval, and a successful formal check establish different things.
We had to preserve those distinctions throughout the backend and interface while keeping the results understandable.
Making the graph usable
Our atlas contains more than a thousand problems. Early visual effects made the graph expensive to render, while opening details could obscure the selected node.
We simplified the connections, reused node graphics, and adjusted camera framing to account for the available screen space.
Keeping useful work when a run stops
Research does not always finish within its token or time budget. We preserve partial findings and failed approaches so an incomplete investigation can still produce something worth examining.
Accomplishments that we're proud of
- Connecting problem discovery, research orchestration, and readable results in one workspace.
- Building a research workflow with independent approaches, shared findings, substantive challenges, and bounded restarts.
- Publishing the trihexagonal shell counterexample with a mathematical explanation and Lean certificate.
- Presenting both an upper bound and a matching construction for the 5×5 grid problem.
- Making the reasoning and supporting artifacts available for inspection.
Our favorite accomplishment is being able to show the actual mathematics behind the result.
The graph is pretty. The contradiction is prettier.
What's next for Triviality
We want to make longer investigations easier to continue, compare, and audit.
Our next priorities are:
- Better recovery and resumption for interrupted research jobs.
- Stronger retrieval across mathematical literature.
- Clearer review of model-generated formal statements.
- Evaluation against single-agent baselines
- More published investigations with reproducible artifacts and explicit verification scope.
We want Triviality to become a workspace where mathematical ideas can be explored seriously, challenged constructively, and checked carefully.
Built with
Next.js · React · TypeScript · Tailwind CSS · Three.js · KaTeX · Node.js · Python · MongoDB · Redis · openJiuwen SwarmFlow · OpenAlex · Lean 4 · Mathlib
Log in or sign up for Devpost to join the conversation.