-
QED: A Multi-Agent System for Mathematical Discovery
Introducing QED, an open-source multi-agent pipeline that transforms mathematical problem statements into rigorous proofs—and solved an open research problem in PDEs
-
pdf-to-Lean: Automatically Formalizing Mathematics from Textbooks
An open-source pipeline that converts mathematical PDFs and LaTeX into verified Lean 4 formalizations
-
Building a Low-Latency News Trading Agent
An open-source AI agent for real-time financial decision-making that processes news and executes trades within 1.5-2 seconds
-
Proofread: A 5-Phase Agent Pipeline for LaTeX
What my Proofread agent is, what it does, and how the 5-phase LaTeX proofreading pipeline works.
-
Forward looking: How powerful the foundational models will be at the end of 2026.
A forward-looking prediction on frontier model capability in advanced mathematical reasoning and proof verification by the end of 2026