2026 · 09 · 092026-09-09September 9, 2026
By Matthew Diakonov and Belinda Mo · Sundial ResearchBy Matthew Diakonov and Belinda Mo, Sundial Research
We built a harness that makes Lean 4 formalization run on autopilot inside a LaTeX editor. A researcher writes their paper as usual; in the background, agents translate the math into Lean and prove what they can. As you write, your work gets checked.
2026 · 06 · 192026-06-19June 19, 2026
By Belinda Mo and Florent Tavernier
Increasingly, people can't explain what their agents did for them. We built Sundial so humans stay at the center of the work: a collaborative workspace where humans and agents edit the same files live, and every change can be reviewed at an exact level of granularity.
2026 · 06 · 142026-06-14June 14, 2026
By Belinda Mo · ICML 2026 position paperBy Belinda Mo, ICML 2026 position paper
AI systems are becoming autonomous research agents, and the verification gap between scientific output and our ability to check it is widening. We argue science must evolve its verification infrastructure: observable-by-default workflows, tiered verification, and clear attribution.