Mathematics and validation
Open Problem Gallery
Portable mathematical strategy graphs, formalization workflows, and distributed human judgment.
Available now
Lean formalizations and independent review
OPG and the Vault render Lean formalizations as read-only cards and provide a user-initiated link to the community Lean playground. In OPG, each formal check and its independent community reviews stay together in the claim's discussion, while server-governed gates determine what public status may follow.
Strategic.GG does not currently execute Lean. Reviewers rerun the code themselves and separately judge whether the formal theorem matches the natural-language claim.
Planned
Portable graph interchange and exports
A faithful Strategic.GG graph file plus publication and editing handoffs for paper-diagram JSON, DOT, Mermaid, SVG, TikZ, and quiver. Each format will state what it preserves and what it drops.
Exports will not turn a visual status snapshot into a proof certificate.
Planned
Lean Blueprint interoperability
Export an OPG dependency plan into a human-reviewable Blueprint starter, then preview pinned Blueprint imports in the authenticated Vault Draft Graph before any publication.
Blueprint progress markers remain source provenance. They do not automatically create OPG verification or standing.
Planned
Strategic.GG-operated Lean service
Move beyond today's reliance on the community Lean instance once sustained use and subscriptions can support dedicated infrastructure. A Strategic.GG-operated service would give the platform control over reliability and the supported size of formalizations.
This is an accepted, usage-gated direction, not functionality currently in development.
Exploring
Pinned machine-check receipts
Record whether the exact submitted code checks against a named Lean environment, together with its source hash, toolchain, and diagnostics.
A machine receipt would answer the formal question only. Independent reviewers would still judge whether the theorem matches the natural-language claim and whether its assumptions are appropriate.
Security prerequisite
Secure external Referee appointments
Domain-scoped Referees can distribute decisive adjudication beyond the founder. External appointments will activate only after opt-in, identity confirmation, and MFA enrollment; decisive Referee actions will also require fresh MFA.
After those safeguards ship, a planned Senior Referee tier would let qualified users appoint ordinary Referees within their own domains. Only the founder would appoint Senior Referees.
The role is accountable mathematical responsibility, not a promotional badge.
Exploring
Evidence-first validation campaigns
Bounded public demonstrations that bind exact claims to reproducible artifacts, machine observations, independent semantic review, corrections, and honest inconclusive outcomes.
Planned
Clearer graphs and finer collaboration
Better mathematical label rendering, more granular node and edge discussion, persistent canonical problems, and contribution signals that help collaborators find useful work without confusing coordination with verification.