13 September 2026

The part of Navier-Stokes no one is talking about

there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as their conventional human-readable proof.

Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook. Then formalizing the 166-page paper from OpenAI would take 132,800 person-hours. It took OpenAI 17 hours to verify their proof in Lean. I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude is revolutionary.
Wow, this is great. Now we have to find mathematicians still willing to continue to pursue mathematics. ☹️ 

––– 良くない–––

Exercise intensity modulates interorgan communication and is associated with cardiometabolic health outcomes in humans. Exercise is still good for you. These scientists identified "intensity-dependent proteins
Integration with a large plasma proteome-phenome repository suggests that sprint-intensity exercise (SIE) acutely stimulates the release of protective proteins into the circulation to a greater extent than moderate-intensive exercise (MIE). These data help explain how SIE, despite requiring only a fraction of the time of MIE, elicits robust metabolic signaling and whole-body benefits.
Sprint-level exercise was six 30-second bouts of cycling against resistance.  Moderate level exercise lasted 90 minutes in the beginning gradually increasing to 120 minutes towards the end. That's a lot of exercise. 😓

––– 凄い –––

It detects Bluetooth signals broadcast by compatible smart glasses and compares their identifiers against a catalogue created by Szydlowski after examining several devices.
Yeah, but what are you going to do about the new Apple Watch that records conversations for playback? There's even an app made for this purpose. It seems that in the near future, everything you do will be recorded.

––– 良くない–––

Open source software is the foundation of a lot of important stuff. It's time we started the conversation about paying for and supporting it. I agree.

––– 凄い –––