Show HN: Browse OpenAI's maths results and compare expert verdicts

Category: other

Tags: lean, mathematics, research-tools, static-site, formal-verification

Score: 6.0/10 (Innovation: 6, Technical: 5, Documentation: 8, Utility: 5)

Plectis Atlas is a static web application that aggregates OpenAI's mathematics papers, their Lean formalizations, and independent assessments from groups like MathVet and cert-machine into a browsable, cross-referenced map. It provides a unified reading experience with paper readers, Lean code viewers, citation graphs, and side-by-side expert verdicts on proof coverage, making it easier to navigate a fragmented research corpus.

Target audience: mathematicians, formal verification researchers, AI safety researchers

Repository: https://wcook04.github.io/plectis-atlas/ · Python · Apache-2.0

View on Hacker News