nicf
No user record in our sample, but nicf has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
No user record in our sample, but nicf has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
Oh, I hope I didn't come off as talking down to you! As I said in another reply here, the intention behind this comment was pretty narrow --- there's a certain perspective on this stuff that I see pretty often on HN…
I certainly didn't mean to dispute that! Formal proofs have a lot in common with code, and of course reading code is illuminating to humans all the time. I meant to be responding specifically to the case where some…
I don't know enough about the RH examples to say what the answer is in that case. I'd be very interested in a perspective from someone who knows more than me! In general, though, the answer to this question would depend…
I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before. I'm actually…
For the articles on my website, I have a pretty janky workflow where I write a LaTeX document that I compile both to a PDF and (using Pandoc) to HTML, which I render with KaTeX. I've been in the market for a while for…
Yeah, that's definitely right --- an explicit counterexample to the Riemann Hypothesis would be very surprising and interesting, and I think that would be equally true no matter whether it was found by a person or a…
Woodworking is very far from my world, so I don't really have any grounds to judge how comparable the two things actually are. I'll say two things instead. First, right now presumably the reason a few people still…
Incomprehensible proofs are indeed still useful to some extent, and I don't think you'll find many mathematicians who would reject them as an answer to the binary question of whether the result is true. But when you…
I was an algebraic geometer when I was still doing research in the field, and it was definitely true in that corner of the world. Authors are alphabetical, and you usually cite the paper by listing them all, no "et…
This is actually a metaphor I've used myself. I do think the woodworking community is both smaller and less professionalized than it would be in a world where industrial furniture production didn't exist. (This is a…
Hm, good question. It depends on what you mean. If you're asking about restricting which theorems we try to prove, then we definitely are cutting ourselves off from vast swathes of math space, and we're doing it on…
This is an interesting question! You're giving me a chance to reflect a little more than I did when I wrote that last comment. I can only speak for myself, but it's not that I care a lot about me personally being the…
oersted's answer basically covers it, so I'm mostly just agreeing with them: the answer is that you use a computer. Not another AI model, but a piece of regular, old-fashioned software that has much more in common with…
I would love that too. In fact, I already spend a good amount of my free time redundantly learning the mathematics that was produced by humans, and I have fun doing it. The thing that makes me sad to imagine --- and…
Especially not mathematicians! No one goes into math academia for the money, and people with math Ph.D.'s are often very employable at much higher salaries if they jump ship to industry. The reason mathematicians stay…
Well, it depends on exactly what future you were imagining. In a world where the model just spits out a totally impenetrable but formally verifiable Lean proof, then yes, absolutely, there's a lot for human…
The Four Color Theorem is a great example! I think this story is often misrepresented as one where mathematicians didn't believe the computer-aided proof. Thurston gets the story right: I think basically everyone in the…
I'm a former research mathematician who worked for a little while in AI research, and this article matched up very well with my own experience with this particular cultural divide. Since I've spent a lot more time in…
Uses what?
I'm a private tutor who works with adults on proof-based math. I've often had a similar thought to the one you're expressing here --- I also found proofs pretty revelatory when I first exposed to them and wondered where…
You're welcome! There's actually one more point that I thought of after sending that reply, which since you mentioned it again I should maybe flag. Totally apart from physics, it may seem intuitively plausible that if…
I'm not sure if this will make you feel any better, but there's an interesting mathematical corner case at work with Norton's Dome that's responsible for the breakdown in the intuition you're expressing in (1). You…
I work as a private tutor for proof-based math, and I have a lot of students who've spent some time self-studying before coming to me. The comment by godelski matches my experience: the biggest obstacle seems to be the…
Nope. Many important results have names that are familiar to everyone in the subfield, so you might say "by So-and-So's Lemma, this module is finitely generated". Failing that, you could maybe cite a paper or a book…
That sounds like a fun and satisfying process! I realize my comment could be taken as denigrating all the people who write about this stuff, but that's certainly not my intention; I've also enjoyed a lot of the…