Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Fermat's Last Theorem – how it’s going

xenaproject.wordpress.com

Post reply on HN
Print view View original

211–216 of 216 posts

Re: Fermat's Last Theorem – how it’s going

#211

Post by pierrefermat1 »

staunton wrote: post #68
lincolnq wrote: post #9

If you're interested in this stuff at all, check out some code. Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M... Also check out the blueprint, which describes the overall structure of the code: https://imperialcollegelondon.github.io/FLT/blueprint/ I'm very much an outside observer, but it is super interesting to see what Lean code looks like and how people contribute to it. Great thing is tha…

Most (larger) Lean projects still have "unit tests". Those might be, e.g., trivial examples and counter examples to some definition, to make sure it isn't vacuous.

I think the better mapping of unit tests would actually be proofs of lemmas ?

Re: Fermat's Last Theorem – how it’s going

#212

Post by [deleted] »

munchler wrote: post #3

> Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer inspection it turned out that the human argument left something to be desired. Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.

[deleted]

Re: Fermat's Last Theorem – how it’s going

#213

Post by staunton »

pierrefermat1 wrote: post #211
staunton wrote: post #68

Earlier quoted context omitted.

Most (larger) Lean projects still have "unit tests". Those might be, e.g., trivial examples and counter examples to some definition, to make sure it isn't vacuous.

I think the better mapping of unit tests would actually be proofs of lemmas ?

I don't see why you would think that.

In such a project theorems and proofs are "the main point of the software". The unit tests make sure certain things don't go wrong by noticing when developers, e.g., mess up while refacing something. Also, people actually put the things I was talking about in a folder called "test"...

Re: Fermat's Last Theorem – how it’s going

#214

Post by ted_dunning »

boothby wrote: post #165
naasking wrote: post #155

Earlier quoted context omitted.

Surely there was angry muttering.

Multiple people raising objections at once, each at a reasonable volume to speak to a large seminar room, and other people speaking to their immediate neighbor. If there was angry muttering, I don't recall it. But yes, a crowd of mathematicians going wild is still pretty chill.

There was a story that Fred Richman got involved in a wrestling match as a result of a disagreement over a proof one time.

I never heard the full story ... everybody in the department at NMSU where he was at the time would just make comments to each other of the form "Remember the time ...?" with a response "Fred's a beast".

Re: Fermat's Last Theorem – how it’s going

#215

Post by ted_dunning »

impendia wrote: post #48
vouaobrasil wrote: post #24

> The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to…

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone w…

I don't think that is a great example since it only takes a moment to see the loose bounds C, X = 3, e.

It would be annoying to have to code that kind of statement every time, but it wouldn't add that much to the effort.

Formalizing is still enormously hard, but I don't think that this is the example to hang the argument on.

Re: Fermat's Last Theorem – how it’s going

#216

Post by ted_dunning »

jebarker wrote: post #102

Formalization of maths seems like an overwhelmingly huge task. A bit like Cyc but harder. Is there some kind of chain reaction likely to happen once a critical mass of math has been formalized so that it becomes easier to do more?

It is also utterly unlike in that the formalization of math actually has real impact. Cyc has never had any impact and almost certainly never will.
Post reply on HN