Pinned Loading

1. quartic-query-lean quartic-query-lean Public

   Lean 4 formalisation of OpenAI's nearly quartic randomized–quantum query-complexity separation, with expositions and a proof reader. Human review of statement fidelity pending.

   Lean 1

2. plectis-erdos plectis-erdos Public

   Papers, proofs and research records for eight Erdős problems, including what is established and what remains open.

   Lean 5

3. proof-reader proof-reader Public

   Read a research paper beside its Lean proof code, with links to exact statements and a diagram of how the proof fits together.

   TypeScript

4. agent-trace-mechanism agent-trace-mechanism Public

   Local Codex and Claude Code session viewer with tool traces, selective context export and optional MCP access. Browser app or native Mac window.

   JavaScript 2

5. code-ontology-bridge code-ontology-bridge Public

   Python static analysis exported to DuckDB, with semantic models for NVIDIA Auto Ontology's text-to-SQL agent. Independent project.

   Python

6. practical-formal-verification practical-formal-verification Public

   Dafny proofs for 16 selected computations in an 88-component research-workflow prototype, with generated Python and coverage maps. Not verification of the complete system.

   Python 3