pfdietz

Previously the stock price was based on expectations, and if those expectations were not met the price could be expected to decline to reflect the actual performance.

> No, what is happening is that the AI is really good at connecting the dots and human mathematicians aren't.

I watched a Zoom presentation yesterday {10/28/2026) at Courant by Maksym Radziwill on the QRH result with the constant 11/12. It used four known ideas, but linked them together in a way that mathematicians had steered themselves away from. He gave a short sentence with four phrases that he said, if they had been sent to him by time machine, would have let him work out the proof years ago. All the details were straightforward once that high level plan was in place.

The advantage AI had here was, in his words, it lacks psychology. Humans had a prejudice that a certain approach would not be fruitful, but the AI didn't have that. The AI could explore superficially unproductive avenues at great depth, not having to do as much pruning to conserve mental effort. And as it turned out one of those approaches worked.

AI is going to fill in a lot of blind spots, I think.

I remember the Motorola Museum on the Schaumburg campus has an Iridium satellite hanging from the ceiling.

The entire museum was demolished a few years ago to make way for a Top Golf.

What's galling is how cheap iodine supplementation is, about $0.02-0.05 per person per year.

Maybe that's the problem. There's no Big Iodine making money to keep politicians paid off.

What do you mean by that?

All that needs to be checked to avoid that is the statement of the main theorem. Any divergence further inside means you proved the main theorem differently than you thought you did -- but you still proved it.

This assumes the Lean kernel itself isn't bugged, but getting it correct is a matter that affects all uses, not just this one, so the cost of making it correct is spread over all those uses.

It's being sunk 20 miles offshore, which is out of Florida control (that extends only nine miles there; which is kind of odd since for most US states the control only extends three miles).

Indeed; one cannot copyright mathematical ideas, only their specific expressions. And the formalization is a different expression.

It's possibly the longest open source project of any kind (depending on whether you count comments and white space in Linux).

The proof was of such complexity and length there were lingering doubts. This dispels them.

Wind certainly helps, but there's a question of what will happen to the relative cost of wind and solar in the future. Solar seems to have a steeper experience curve.

The formalization is 43.1M lines of Lean.

Oh European colonial mindset, don't ever change.