3 ms·

I would strongly assume Buzzard believes those two positions to be perfectly compatible and consistent. I'm sure it would be very insightful to hear him explain

I would strongly assume Buzzard believes those two positions to be perfectly compatible and consistent. I'm sure it would be very insightful to hear him explain how they are. Hope someone asks him about it. > formalization would be a great practical tool to mitigate those problems Yes, I agree. V. Voevodsky's story is a great example how things can go wrong and I very much admire him for the consequences he took from that. However, if some mathematician has the goal of advancing a certain field, I don't think you can argue convincingly in 2023 that they should formalize their papers because making extra sure there's no errors is worth the time investment in terms of advancing the field. Again, I expect to see this slowly change.

t_mann 3y ago
I'm not saying that starting 2024, journals should only start accepting formalized proofs. I'm well aware that we're probably many thousands of person years away from being able to formalize research involving modern mathematical objects like rough paths or perfectoid spaces. But I do think that we should be moving in that direction. We're halfway through formalizing undergrad education, once we're there we could start including it in graduate courses, and at some point we'll have caught up. Many thousands of years of work divided by many thousands of active grad students maybe isn't prohibitively much. I don't see a reason why in some future, something like Lean couldn't replace something like LaTeX as the de-facto standard language for communicating mathematics. We could build the papers directly from source with docstrings. I don't even think that it would replace peer review, since this considers at least three things, correctness, novelty and relevance, roughly in that order, but it could make it substantially easier by automating much of the first part. And I think it might make the paper writing itself more efficient and enjoyable as well.

t_mann 3y ago

I'm not saying that starting 2024, journals should only start accepting formalized proofs. I'm well aware that we're probably many thousands of person years away from being able to formalize research involving modern mathematical objects like rough paths or perfectoid spaces. But I do think that we should be moving in that direction. We're halfway through formalizing undergrad education, once we're there we could start including it in graduate courses, and at some point we'll have caught up. Many thousands of years of work divided by many thousands of active grad students maybe isn't prohibitively much. I don't see a reason why in some future, something like Lean couldn't replace something like LaTeX as the de-facto standard language for communicating mathematics. We could build the papers directly from source with docstrings. I don't even think that it would replace peer review, since this considers at least three things, correctness, novelty and relevance, roughly in that order, but it could make it substantially easier by automating much of the first part. And I think it might make the paper writing itself more efficient and enjoyable as well.