Thread

1. ipdashc · 1790020558 · focus · HN ↗

   I knew mathematicians were a smart bunch, but honestly, the events of the past few weeks have really given me a new level of respect for them.

   They might be the first community I've seen to experience the AI "rush" and (at least as presented to an outside observer) immediately come together, assess the situation, and calmly, empathetically, and rationally act. They evaluated what AI is good at and what it lacks. They've thought through how it'll likely affect their field in the future. They've explained where the need for humans still lies, and made clear proposals for how to change their own field and for what demands to make of AI companies. Of course they're not all on the same page, but they're at least talking and trying.

   They haven't started worshipping the machine god and loudly claiming their whole field is solved. Nor have they flailed wildly at LLMs as if complaining enough about it will make them go away.

   Every major statement I've seen come out of the math community on this matter reads as well thought-through, humble, reasoned, and deeply human.

   In these days of fear, uncertainty, and obsolescence anxiety, honestly, they've given me some confidence that maybe we will figure this stuff out after all. Maybe we'll learn from them. Who knows.

   1. ksd482 · 1790020937 · focus · HN ↗

      Agreed.

      Their field is extremely rigorous. As rigorous as it can possibly get in that they have to prove each and every line of their work beyond any doubt. The discipline they have cultivated in their culture shows in their response to AI as well.

      As opposed to some other fields in which rigor was either not part of the culture or was not always possible. For e.g., software engineering in terms of code quality being produced. There were some indirect signals here and there but they are all subjective.

      1. cubefox · 1790088307 · focus · HN ↗

         In some sense software engineering is more rigorous than mathematics, because proofs are generally informal, apart from those written in Lean, while all computer programs are strictly formal, as otherwise they wouldn't be machine-readable.

         1. ksd482 · 1790187862 · focus · HN ↗

            I see what you are sayings. That's an interesting point of view.

            Perhaps we should define what rigor means.

            Your point is that code is executable and speaks for itself whereas a Math proof (non-lean) is just someone's writing on a piece of paper.

            Now let's compare the "practice" of doing Math and software engineering. In Math, every step is very intentional, and getting to a point where a proof is complete and correct is a very long, laborious, difficult and intentional process. Not to mention, the work is also peer reviewed (for published stuff). This is what I mean by rigor.

            In software engineering, the practice is quite different. We defined the problem (somewhat), come up with a design that we "think" would work, write programs that we think is correct and then execute it. Most of the time it doesn't work exactly as we would have predicted. So we take the signal and adjust. So it's a more iterative part and this gets us closer to reality (what we actually want it to be), step by step.

            So comparing the two, the major difference I see is in one each and every step is very intentional and we can't guess it. While in the other one we have lots of liberties, but we are still making progress.

            So to me the difference is just between the practices followed in the field when it comes to rigor.

            1. cubefox · 1790196848 · focus · HN ↗

               Maybe a similar comparison would be this: for proofs, the standards of correctness are purely internal and can in principle be formally defined, as in Lean. The formal conjecture has to follow from the premises. Either it is proven or not. In contrast, in 99% of ordinary software, no fully formal standard of correctness exists. The requirements are informal. So what counts as a bug and what doesn't is a judgement call that can only be checked by asking the person who wanted the software whether it works as intended.

Unofficial Hacker News client; not affiliated with Y Combinator.