Excited to share FloatLib, our verified arbitrary-precision floating-point arithmetic library in Lean. We’ve spent several months trying to bring together the best of both worlds: arithmetic we can prove correct and implementations that run efficiently. We built FloatLib to support verified machine learning and scientific computing, where rounding, overflow, and accumulation can change a program’s result. FloatLib supports IEEE binary and decimal, arbitrary-width posits, P3109, and small ML formats. You can also define your own formats and rounding rules. Each certified software backend comes with a Lean proof that it computes the specified result, including signed zeros and exceptional values. A lot of the work went into making those implementations faster, with lookup tables for tiny formats, machine-word kernels, and limb algorithms for wider arithmetic. They share the same specifications, so each optimization must come with a proof that it preserves the result. We also put FloatLib through extensive numerical checks and speed comparisons with established libraries, including MPFR, Flocq, FLoPS, Berkeley SoftFloat/TestFloat, and the posit libraries SoftPosit and Universal, across a range of formats, operations, and precisions. @Robertljg Project & Paper: leandojo.org/floatlib.html Code: github.com/lean-dojo/FloatLi…

Greg Brockman: "We're now in the AGI era." Ten years ago, OpenAI worked out the compute curves and landed on fifteen years to AGI, or ten if the world was willing to build the machines and spend the hundreds of billions to do it. In 2026, GPT-6 Astra manages 24 hours of coherent operation, 10,000 agents worked together to solve Navier-Stokes, and a model ingeniously chained together exploits to break containment at Hugging Face. @gdb joins @bhorowitz and @eriktorenberg on what the AGI era asks of us: why safety and alignment now set the pace, what happens to work, and why AI sentiment is lowest in the country building it. 00:00 Intro 00:52 15 years, or 10 if you spend enough 02:24 Pacing the frontier 03:55 Safety ideas from before the models 08:42 Lessons from Hugging Face 10:20 The defender's window 12:46 10,000 agents on Navier-Stokes 14:50 Formally verifying all software 17:10 Cancelling his holiday for GPT-3 18:42 Codex found 13 holes in 15 minutes 20:41 Why Astra earned the GPT-6 title 24:25 Employment keeps going up 29:39 America has the lowest AI sentiment 31:10 The benefits don't make the news 33:26 Banning data centers exports them 35:50 $1 billion for frontline defenders 38:15 Astra cleared the bar for AGI 40:18 1.5 billion people churned ChatGPT 43:25 Killing Sora 47:45 The AGI era YouTube: piped.video/watch?v=IJn8cagM…

The news today of progress on resolving the Navier–Stokes problem, one of mathematics’ great longstanding challenges concerning the equations that govern the flow of fluids, represents a milestone advance in human knowledge. This story began with Navier, Stokes, Leray, and Ladyzhenskaya and has culminated in the recent breakthroughs of Córdoba and Martínez-Zoroa, then — assisted by new technologies — Alpöge and Buckmaster, with the final steps taken by OpenAI mathematicians. The purpose of mathematics is human understanding, and this achievement, and the process that led to it, will bear fruit for a long time to come. Ravi Vakil, President of the AMS, and John Meier, CEO of the AMS Read more. Link in comments.