The Open Problem Gallery: Coordinating Mathematics Research

Why I built the Open Problem Gallery

I wasn’t trying to diagram finished mathematics after the fact. I wanted the search itself—claims, dead ends, checks, forks, challenges, and reversals—to leave an inspectable record. Once the search becomes legible, coordination can scale: people can see what has already been tried, what remains unresolved, and where their effort can matter.

That desire was personal. In graduate school, I wanted to spend several years trying to reach the frontier of mathematics and contribute there, even though I did not expect academia to be my permanent home. I was aiming toward topology and topological data analysis before I left graduate school to work as a trader. The conventional record of those years—a CV, a specialization, and papers on arXiv or in journals—made sense inside academia. Outside it, much of the process disappeared.

The transition worked out fine. The private sector recruits analytically minded STEM graduates every day. My frustration was narrower. A publication list did not show the problems I had tried, the approaches that failed, the claims I had checked, the collaborative work that never became a paper, or the judgment I had developed along the way. A résumé could describe those things, but description is still self-report.

The Polymath Project showed me what open mathematical collaboration could feel like. But openness and visibility were not enough. A graph can show how claims depend on one another; it cannot tell you which claims have earned standing. A forum can collect opinions; it cannot, by itself, distinguish a bare assertion from a claim that has cleared a defined process. OPG asks what happens when those collaborative moves become explicit—and when the platform enforces what counts as evidence, what counts as a challenge, and what must happen before either can change a claim’s public standing.

That is the rating-grind instinct behind OPG: standing should emerge from inspectable work, not from popularity, résumé, confidence, or self-description. The graph records the search; the checks, challenges, contested states, adjudication, and lineage give that record consequences. I did not want a score for time spent or credit merely for trying. I wanted evidence of how someone approached difficult problems—and of what happened when other people checked, challenged, or built on that work.

Proof of strategy was my answer. But it only works if it is more than a richer résumé. If authors can assign their own standing, the original problem returns. That is why OPG separates the judgment an author is free to express from the public standing that can follow only from the platform’s process.

Author judgment versus public standing

I wanted authors to retain the right to state their own conclusions. When you publish a claim, you can mark your own read as verified or falsified. That annotation remains visible because the author’s judgment is part of the record. OPG does not need to erase that judgment to distinguish the author’s read from the claim’s public standing.

But being allowed to state your conclusion is not the same power as being allowed to award yourself standing for it. On OPG, verified and Formally Verified intentionally mean different things. The first says, “This is the author’s read.” The second says, “A formal check has received the required review and has been attached to this claim through OPG’s rules.”

When a claim still needs a formalization, anyone viewing it can use Request link to invite one. The link opens the problem with that claim selected and the formal-check composer ready. It is only a coordination tool: copying or opening the link creates nothing on OPG and does not change the claim’s status.

For a claim to display Formally Verified, someone must first post a verifies formal check in that claim’s Selected discussion. The post contains the Lean code—including the formal theorem statement—and identifies the claim it addresses. It remains alongside the other comments and reviews for that claim. Reviewers corroborate that specific formal check, not a general description of the work. If its text, declared outcome, or target changes, the earlier corroboration no longer counts.

Once the check has enough qualifying support, the problem’s author can select Mark node Formally Verified on that check. Before changing the claim’s public status, OPG checks again that the check still belongs to that problem, still targets that claim, still declares verifies, still has qualifying support, and is not blocked by a decisive refutation. Only then does the claim display Formally Verified.

A Request link merely invites someone to contribute a formalization, and an author’s own verified annotation merely states the author’s conclusion. Neither can produce Formally Verified. An author may be right before the process is complete, so the absence of that label does not mean the author is wrong. It means the required check, review, and attachment are not all in place. OPG preserves the author’s judgment without laundering it into a credential.

Formally Verified is therefore not an oracle’s declaration of eternal truth. It tells readers that a specific verifies formal check received the required support and was attached to that claim under OPG’s current rules. The claim can later become Formally Contested or Formally Falsified. None of those formal-status labels changes the numeric Influence score.

Why independent corroboration matters

Once the author’s judgment is separated from the claim’s public standing, another temptation appears: treating a Lean formalization as self-explanatory. It is not. For a verifying check, I want three questions kept separate:

1. Did the submitted Lean code check successfully?

2. Does its formal statement match the natural-language claim attached to the node?

3. Are its assumptions, axioms, provenance, and dependencies acceptable?

A successful answer to the first question does not settle the other two. Lean checks whether a formal proof establishes the formal statement it was given. It cannot decide whether that statement faithfully represents the claim readers saw, whether a hidden assumption changed its meaning, or whether the formalization was attached to the right node.

That is why independent corroboration matters. Lean and human reviewers answer different questions. Lean checks whether the submitted code proves the formal statement it contains. Reviewers check whether that statement matches the claim readers were asked to believe and whether its axioms and assumptions are acceptable. A valid Lean proof can still establish something weaker, narrower, or different from what the surrounding prose appears to claim.

Strategic.GG does not currently run Lean, and displaying Lean code is not the same as checking it. Reviewers rerun the submission in their own Lean environment. They report whether it checked successfully, contained errors or sorry—Lean’s placeholder for an unfinished proof—relied on unexpected axioms, and matched the natural-language claim. Strategic.GG records what those reviewers report; it does not present their reports as results from an in-platform proof checker. This is a launch constraint, not the intended endpoint. I plan to run Lean on Strategic.GG’s own infrastructure once traffic and subscriptions can support the cost; I’ll track that work on the development roadmap. That would let the platform check submitted code directly and support larger formalizations than the current playground handoff can reliably accommodate. Independent reviewers would still determine whether the formal theorem matches the natural-language claim.

To identify exactly what was reviewed, OPG gives each formal check a digital fingerprint, called a hash. That fingerprint represents the submitted code, whether the check says verifies or refutes, and the particular claim it addresses. If any of those changes, the fingerprint changes too. Earlier reviews remain part of the history, but they no longer count as reviews of the new version.

A review from the person who wrote the formalization or the author of the problem can still be useful and remain visible, but it does not count as independent support. In the community-review path, qualifying support must exceed qualifying needs work reviews by at least two. Two supporting reviews and no needs work reviews qualify; three supporting reviews and one needs work review also qualify. Two supporting reviews and one needs work review do not.

These are community reviews, not Referee ballots. Community reviews determine whether a formal check has been independently examined and has enough support to qualify through the community path. A Referee ballot is a separate vote cast by someone authorized to judge formal checks in that mathematical domain. Referee ballots can change a claim’s formal status.

Independent corroboration therefore does not make a claim infallible. It creates an inspectable chain of accountability: the exact claim, the exact formalization, the exact version, who examined it, and what they reported.

Why Formally Falsified requires two Referee ballots

I wanted disagreement to be easy to publish. Any contributor can submit a Lean formalization as a formal check marked refutes. This means the submission is intended to show that the claim is false—for example, by giving a counterexample or proving its negation. Marking it refutes does not make that conclusion official. Community reviewers examine whether the Lean code checks and whether its formal statement actually refutes the claim written in ordinary mathematical language.

If a challenge against a Formally Verified claim qualifies through the community path, the claim can instead display Formally Contested. Readers can therefore see that serious counterevidence exists before the Referee process has reached the stronger status change.

The two stages answer different questions. Community review asks whether the challenge has enough independent support that readers should be warned. Referee review asks whether the evidence warrants changing the claim from Formally Verified to Formally Falsified. Community review can produce the warning; it cannot make that reversal.

I chose different thresholds within the Referee process. One eligible Referee ballot can approve a verifies formal check, turning it to Formally Verified. Replacing Formally Verified with Formally Falsified requires two currently valid ballots approving the same refutes formal check. Each ballot approves one exact formal check; it is not an abstract vote on whether the claim feels true or false.

The intended ordinary path is for two appointed domain Referees to supply those ballots without me. The software also permits my founder account to supply one ballot during the system’s cold start, but never both. One appointed Referee must still agree. I do not treat that permission as mathematical authority, and I do not intend to vote on ordinary mathematical questions once qualified Referees are available.

Each voter must also be independent of the work being judged. Neither may have submitted the formal check, be the problem’s author, or have supported that same check as a community reviewer. These rules prevent someone from helping create or corroborate the evidence and then judging it at the ballot stage.

Requiring a second ballot affects only the change to Formally Falsified. The refutes check and its community reviews remain visible while that decision is pending. Before changing the status, OPG checks that both ballots still approve the exact version under review, that neither ballot has been withdrawn, and that both voters remain authorized and independent. If any of those conditions is no longer true, the ballot stops counting.

OPG also refuses to choose automatically between opposing decisions at the Referee level. If an existing verification has already received founder, Referee, or machine approval and a refutation later receives two ballots, the claim remains Formally Contested.

The founder account currently has a protected conflict-resolution control capable of breaking that deadlock. I regard it as an emergency security power, not a mathematical court of appeal. I intend to use it only when the record shows that the process itself has been compromised—for example, through a compromised account, a disqualifying conflict, coordinated abuse, or a security incident. If qualified Referees disagree in good faith about the mathematics, Formally Contested is the honest status. I will leave that disagreement visible rather than appoint myself the final judge. An independent appeals process remains future governance work.

At initial public launch, my founder account will be the only ballot-enabled account. That is a cold-start security arrangement, not a claim of mathematical authority. I will not activate external Referees until the planned identity-confirmation, acceptance, and two-factor-authentication protections are implemented. Until then, the two-voter Referee path to Formally Falsified cannot be completed. That does not block OPG’s release: contributors can still publish challenges, and a qualifying community-reviewed challenge can still place an existing Formally Verified claim under Formally Contested.

Once those protections are in place, I will initially control Referee appointments. That is an access-control responsibility, not authority over how Referees should vote. Two appointed Referees will be able to complete an ordinary falsification without me. A later update will add Senior Referees who can appoint ordinary Referees within their domains. As participation grows, my role should narrow to protecting the process from compromised accounts, coordinated abuse, and security failures—not deciding which mathematical argument wins.

OPG therefore lets contributors publish challenges, lets independent community review warn readers, and requires agreement from two different eligible voters before reversing a claim’s status. Building the platform does not make me a mathematical court of last resort. When qualified people disagree and the process has not resolved that disagreement, Formally Contested is a result, not a failure.

Humans and agents together

Bot-first does not mean bot-sovereign. OPG is bot-first because its API describes the available actions in machine-readable form and lets an agent perform most of the same constructive actions available through the website. After a one-time token setup, the website becomes optional for constructive work: you can map claims, submit formalizations, review checks, cite, fork, and challenge entirely through an API-capable agent in your preferred LLM environment. Every action is attributed to your account and passes through the same server checks and account-level limits. Agent contributions are not treated as second-class work, but they receive no special authority either.

Those actions can contribute evidence, but no submission changes a claim’s status by itself. An agent may submit a verifies or refutes formal check. Once a verifies check qualifies, an agent acting for the author of the problem can select it as the evidence supporting that claim; OPG rechecks every gate before displaying Formally Verified. Changing a claim to Formally Falsified still requires the Referee process described above. An agent can help build and examine the case, and it can perform the author’s selection step, but it cannot cast a Referee ballot or resolve a formal contest.

Lean also has a specific job. When someone runs a formalization in Lean, Lean checks whether the code establishes the formal statement it was given. Lean does not decide whether that statement matches the natural-language claim, whether its assumptions are acceptable, or which status OPG should display. Those decisions remain part of OPG’s community-review and Referee processes.

The dividing line is therefore between contribution and adjudication, not simply between humans and machines. An ordinary user does not gain Referee authority merely by contributing. Referee ballots are available only through separately governed human accounts, and the token API provides no action for casting one or resolving a formal contest. An agent therefore cannot exercise those powers, even when acting for an account whose owner is a Referee.

Several agent tokens also cannot manufacture independent support. If one user delegates five agents, all five still act through the same account and count as one identity. Creating more tokens cannot manufacture several reviewers or satisfy a quorum. This is more than keeping a human “in the loop.” Contribution and adjudication have different keys.

Don’t take my word for it

The problem was not a lack of mathematical tools. It was a lack of shared memory between them. Formalizers already work across local Lean environments, GitHub, Zulip, Blueprint, and other tools. They should keep working where they work best. OPG is not another IDE or proof checker. It gives that distributed work a common context: which claim a formalization supports, where the claim fits into the larger strategy, who checked it, what challenged it, and which formal-status label, if any, it currently displays.

OPG is community infrastructure, but it also gives individuals a reason to contribute. I wanted a place where people could show off—but show off the right thing. Not follower counts, job titles, or polished self-descriptions. The stronger record is the problems you chose, the moves you made, the evidence you attached, how you responded when challenged, and what remained standing after scrutiny.

That is what I mean by proof of strategy. For someone working with agents, it is not proof that they did everything without AI. It is evidence that they used powerful tools without outsourcing judgment. The contributor gains an inspectable public record of their work; the community gains knowledge that other people can find, check, challenge, and build on. If those incentives reinforce each other, they can support a more self-organizing research ecosystem.

But don’t take my word for the system. Go to the Open Problem Gallery and pick one claim with an attached Lean formalization. Compare the formal theorem and its assumptions with the natural-language claim. Try to find the first place they diverge. You can use your own Lean environment or ask an agent to help, but record what you actually checked. If it holds up, record exactly what you checked. If it fails, show exactly where.

If you prefer to work through an agent, paste the API documentation—not the token—into your preferred LLM, then configure the agent to use an API token generated from your Settings page. The agent can map claims, submit formalizations, review, cite, and fork on your behalf under your account’s limits, but it cannot cast Referee ballots or resolve a formal contest.

If you have subject-matter expertise and would be interested in serving as a domain Referee once the required 2FA protections are in place, contact me at mercury AT strategic DOT gg. Mathematical judgment should be distributed among qualified, accountable Referees. My role is to protect the integrity of that process, not to decide the mathematics.

That is how OPG should prove itself: not through a launch claim, but one exact claim, one exact formalization, and one accountable review at a time.