In 2023, #Amazon AWS poached #LeonardoDeMoura (the designer of Lean theorem #prover and #programming language) from #Microsoft Research. That sure was a coup.
https://www.amazon.science/blog/how-the-lean-language-brings-math-to-coding-and-coding-to-math
@dougmerritt Surely. If I were, I wouldn't be talking about Lean so much. AWS is now all-in on software verification. It'd be interesting, over the next few years.
The main point I was trying to make (but clearly failed) was this: it used to be that the rich funded academic research via donations to academic institutions, but now they control the research institutions completely.
The billionaires now control our political system, our court systems, our education system, our media outlets, our financial system, and our national defence. And they track every aspect of our lives, financial, personal, professional, the lot.
This is no recipe for progress; it's the prescription for regress back to the pre-Renascence Europe.
Truth be told, it must be an exceedingly dull life for a person to be brooding on a $500B hoard, just to hatch more of the same—life loses meaning, when one possesses that much resources. Meanwhile, on the other side of the world, billions struggle mightily, to forestall starving just one more day.
@AmenZwa Hopefully they can fix it. Lean looks like Haskell written in Python except harder to read
theorem append_length (xs ys : List a)
: (append xs ys).length = xs.length + ys.length := by
induction xs with
| nil => simp [append]
| cons x xs ih => simp [append, ih]; omega
amen zwa, esq.
DougMerritt (log😅 = 💧log😄)
CubeRootOfTrue