Logician, musician, special edition. I run upper division math at Chaminade University, and study computability theory/LEAN when I can. Opinions my own. He/him.
Honolulu, HI
Joined June 2021
- Tweets3.2K
- Following34
- Followers288
- Likes60.2K
That’s an argument that mathematical concepts are esoteric (which is true), not that eigenspaces are esoteric within the category of mathematical objects (which is false).
The sentence is unfortunately ambiguous. I’d’ve just cut the word
I just think a hundred years of mathematics (including work by those determined to find fault with ZFC!) should push one’s credence above 75%.
My point is the vast majority of mathematics can be formalized in ZFC, and that we’ve known this for a while. We get to breathe easy and work off vibes.
Conversely, if the vibes are ever rancid, that could translate to a problem in ZFC. But that hasn’t happened!
Even without all tools a modern logician can bring to bear on the question, 75% on Con(ZFC) seems insanely low for any working mathematician.
A one in four chance that in a hundred years of working in ZFC, no one’s spotted the problem? One in FOUR?
David J. Webb retweeted
A pessimistic hypothesis for complexity theory: every simple and beautiful algorithm can be made log(n)^epsilon faster by making it incredibly ugly
David J. Webb retweeted
An internal model at OpenAI has produced a claimed refutation of ETH! Russell Impagliazzo, Mohan Paturi, and I have been asked to help organize an open and independent examination of this claim. 1/4
David J. Webb retweeted
OpenAI claims that the Exponential Time Hypothesis is false, solving 3SAT (even counting the number of solutions) in 2^{o(n)} time, with a Lean formalization of the proof.
Announcement: openai.com/index/building-sc…
Paper: github.com/openai/math/blob/…
1/2
He seems (at least in this episode) to think that his life is not worth living if he is not Captain of the Enterprise. So my read was that his life (in the actual timeline) to that point was in pursuit of advancement until he settled into that role.
David J. Webb retweeted
TBF Lean’s rise had little to do with dependent types. Rather, its pleasant UX turned a few mathematicians into enthusiasts who built a library of mostly… classical math, which in turn spurred unprecedented adoption by stars like Terence Tao.
This is a good point - and I agreee biology is harder than AI evangelists claim - but it’s slightly at odds rhetorically with the fact that computers have been better than humans at Go for a while. The lesson seems to be that you don’t need perfect simulation to do good work!
I mean, he says Picard doesn’t stand out as an officer, but that he’s a solid member of the crew that they’d be sad to lose.
Serving on the flagship of the fleet is a great life, even without promotion. It’s just not enough for Picard, because he’s ruthlessly ambitious.
I disagree!
“What is randomness, really?” and “What are the limits of computation?” are reasonable philosophical questions that have been resolved to almost universal satisfaction by mathematical logicians.
Sure, there are quibbles on the margins, but that’s philosophy for you.
Like Busy Beaver numbers and the smallest known Turing Machine that halts iff ZFC isn’t consistent, it’s just neat!
That would make it sound a little stranger in plain English but it would make the underlying logic more straightforward logically (as is so often the case!)