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.3K
Perhaps poor phrasing on my part. I’m referring to the rate of convergence issue - while we have a formula which converges, we don’t know how quickly, so we cannot approximate the area to a desired precision.
At first I was very annoyed that we don’t know this, but upon further reflection it makes perfect sense that it’s a problem of precision
I hear they’re gonna be huge nitter.gq/littmath/status/211525…
Evergreen
nitter.gq/littmath/status/205742…
Maybe? I will have to check. This week I am very busy so I’m not a good choice if you want to push it out sooner rather than later 😅
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.
