That seems like a red herring. Have you independently verified the human generated proof of FLT? Surely someone else will try to verify Anthropic's formalization on different hardware. Plus, it seems likely that FLT formalizations will improve / get shorter over time, requiring less compute. And computers (and type-checkers) will continue to get faster over time as well. So maybe in 5 years you could own a computer fast enough to verify a/the proof in say a week, instead of 5 hours.
This feels backwards. I frequently joke "physics is the subset of mathematics that reflects the observable world". Math can be as abstract as it wants, but physics has a constraint. It must model an observable world (related, this us part of why people say String Theory is math and not physics)
PWDR. Why doesn't satellite get around whatever blocks Iran has in place? Are they able to effectively able to jam everything? Seems like the U.S. should be paying the satellite providers to give away "free" service in Iran. Maybe there are just not enough receivers and they are too expensive? Plus, maybe a summary execution if caught with a receiver. Maybe the U.S. should be doing air drops of satellite receivers.
For Iran, this is an extitential moment for an ancient culture, and therefor descisiins are bieng made based on what consitutes any part of that threat, and since they have a much greater technical capacity than say, Afganistan, they are doing a flex on the internet, perhaps heading towards something like a cross between the great firewall and minitell.
And then there is the simple reality of the internet as a whole bieng a putrid swamp that the rest of the 'free' world is trying to grapple with anyway, and it is very very difficult to point to how loosing access to the internet is realy that bad.
If they can , along with many other countrys, solve banking and business, and ditch the swarm of media/porn/extreamist/gambling shit shows, then you can count on that bieng
a goal that many people here will get on board with, rather than find fault in, which goes a long way to explaining the exceptionaly tepid response to the internet going down there, in fact the response here borders on the the whistfull.
Satellite tech like Starlinks need either very visible dishes, or in Starlink's case, local ground stations, to operate. I'm sure there are Iranian ground stations though, just that they're configured to mine crypto or obscure hacking attempts by government-backed groups.
People also need to be cautious with potential adversarial proofs. Like don't decide to give money on a sure-bet thing, just because they have a Lean proof. Not saying that these AI labs would do this.
In a similar vein, where does the theorem statement even reside, just so we can take a look at how large that is? Is it the four files with "Theorem" (and no "Comparator") in the file name? ("R3/Theorem.lean", "LocalPaperTheorem.lean", "PeriodiocPaperTheorem.lean", and "WholeDomainPhysicalStageTheorem.lean").
What is your estimate for the number of hours to formalize one page of undergraduate mathematics? Maybe you are saying this is close to zero, if/when Mathlib eventually covers all of undergraduate math?
Kind of odd that I haven't seen him mentioned in any of these discussions. How does Ted Kaczynski fit into all of this?
* He was correct
* He was wrong
* He was correct, but for the wrong reasons
* He was correct, but too extreme
* He was correct, and not extreme enough
* He was correct, but too early
* He was correct, but unpleasant as a person
* I haven't read the manifesto, but I have strong opinions anyway
* Ted who?
You mean Jacques Ellul? Ted Kaczynski was heavily influenced by little known French Philosopher / Anarchist Ellul's anti-technology books. Ted even mentioned this to his prison interviewer. Here is a copy of Ted's 1983 letter to Ellul:
Ted always seems to get the recognition for being the main, or original, anti-technologist who "foresaw" our modern predicament because he killed people to make enough noise to get his manifesto published. Ellul and many others were before him.
The Netflix documentary on Ted Kaczynski is real good.
reply