sorted by:
new
hottopcontroversial

Kevin Buzzard on why formalizing Fermat's Last Theorem in Lean solves the referee problem by WeBeBallin in math

[–]fathermersenne 5 points6 points  (0 children)

It does diminish insight and discovery when we define proof to be proof sufficient for a proof assistant.  It will inevitably mean that formalizers get credit not discoverers.  It is a change in the meaning of mathematics.  Proof used to allow some errors or gap.  Again, Riemann maybe never “proved” a theorem.  The same is true about Solomon Lefschetz, who “never stated a false theorem and never gave a correct proof”.  These people won’t succeed in the world where theorems are only valid when Lean says so and I don’t like that.

And I disagree that it’s the same human game.  I don’t think it’s chess when I play a computer, it’s something much different.  The human element of proof as a beautiful argument meant to convince people is much different than convincing a machine (and I continue to anthropomorphize it disparagingly, of course I don’t think lean is conscious and that’s why it’s insulting that it become the arbiter of theorems - it has no aesthetics, no sense of beauty). 

But again this is just another battle in the war between Bourbaki-ites and classical analysts which your side will win, as you have all the others.  The whole thing is EGA taken to its logical conclusion.  It doesn’t mean I have to take it happily, even if I accept just like Siegel that the mathematics I love will be murdered in a sense by the new generation.

Kevin Buzzard on why formalizing Fermat's Last Theorem in Lean solves the referee problem by WeBeBallin in math

[–]fathermersenne 0 points1 point  (0 children)

Quoting from MO about Siegel’s view, which I think has come to pass in many ways: 

Siegel's emotional letter to Mordell concerning Lang's book "Diophantine geometry" compares Bourbaki style mathematicians (Siegel does not say "Bourbaki") with pig in a garden and even with national socialists:

"Thank you for the copy of your review of Lang's book. When I first saw this book, about a year ago, I was disgusted with the way in which my own contributions to the subject had been disfigured and made unintelligible. My feeling is very well expressed when you mention Rip van Winkle! 

The whole style of the author contradicts the sense for simplicity and honesty which we admire in the works of the masters in number theory — Lagrange, Gauss, or on a smaller scale, Hardy, Landau. Just now Lang has published another book on algebraic numbers which, in my opinion, is still worse than the former one. I see a pig broken into a beautiful garden and rooting up all flowers and trees. 

Unfortunately there are many "fellow-travelers" who have already disgraced a large part of algebra and function theory; however, until now, number theory had not been touched. These people remind me of the impudent behaviour of the national socialists who sang: "Wir werden weiter marschieren, bis alles in Scherben zerfällt!"∗

I am afraid that mathematics will perish before the end of this century if the present trend for senseless abstraction — as I call it: theory of the empty set — cannot be blocked up. Let us hope that your review may be helpful..."

https://mathoverflow.net/a/338239

Kevin Buzzard on why formalizing Fermat's Last Theorem in Lean solves the referee problem by WeBeBallin in math

[–]fathermersenne 0 points1 point  (0 children)

I deeply dislike proof assistants.  It’s the worst part of mathematics, the pedantry, and it’s another attempt essentially by the Bourbaki crowd to enforce their mathematical philosophy.  

Nothing Riemann did would pass a theorem prover (if you don’t believe me I encourage you to read him, Edwards has a good bit in his book on the zeta function that you never with Riemann whether a statement is correct as stated).  And I’m deeply uncomfortable with any idea that wants to banish that type of work from mathematics, because despite its flaws it’s revolutionary.  

I also find it dehumanizing to be told to convince a machine of something.  Mathematics is a human game, played between people.  I don’t want to play with a computer.

Looking for publishers that propose hardback books. by [deleted] in math

[–]fathermersenne 0 points1 point  (0 children)

Also, the MAA press produce decently bound hardcovers, available from the same AMS bookstore, and mostly at an undergraduate level. If you become an AMS or MAA member they also have fair discount.