[HN Gopher] A Rosetta Stone for Mathematics: Andre Weil's 1940 l...
___________________________________________________________________
A Rosetta Stone for Mathematics: Andre Weil's 1940 letter
Author : pseudolus
Score : 65 points
Date : 2024-05-06 23:46 UTC (23 hours ago)
(HTM) web link (www.quantamagazine.org)
(TXT) w3m dump (www.quantamagazine.org)
| maCDzP wrote:
| What, Simone Weil the philosopher and Andre Weil are siblings?
|
| That's really cool.
|
| I can recommend Philosophy This podcast on Simone Weil for those
| interested.
| rolandog wrote:
| Chiming in with a suggested correction:
| s/Philosophy/Philosophize/
|
| And, totally agree with the episodes (#172-#175) being worth
| multiple listens. They're that good.
| robinhouston wrote:
| I assume the reason this article has been published this week in
| particular is that a proof of the geometric Langlands conjecture
| has just been announced. [1]
|
| The first paper in the series was posted to the arXiv yesterday.
| [2]
|
| It's obviously far too soon to say whether the proof is correct,
| but I'm sure experts will be taking a keen interest.
|
| 1. https://people.mpim-bonn.mpg.de/gaitsgde/GLC/ 2.
| https://arxiv.org/abs/2405.03599
| CobrastanJorji wrote:
| You know, it's always kind of bothered me that we constantly
| run into these "it's far too soon to say whether the proof is
| correct" issues. They're proofs. It should be apparent whether
| they are correct. Otherwise, are they really proof? As a layman
| who's only familiar with Hilbert's work as it pertains to Godel
| and CS, I'm curious what makes expressing these proofs using
| some sort of formal logic so difficult.
| interiorchurch wrote:
| > As a layman who's only familiar with Hilbert's work as it
| pertains to Godel and CS, I'm curious what makes expressing
| these proofs using some sort of formal logic so difficult.
|
| For one thing, they'd be _much_ longer, and likely not human-
| readable.
| phlofy wrote:
| Proofs are literature. They need to go through a peer review
| process to have someone other than the author verify their
| correctness. Nowadays often tools like Lean are used to
| convert the argument into what you would call formal logic.
| It's nontrivial and takes time.
| robinhouston wrote:
| In this particular case, the proof literally hasn't been
| written up yet! The papers are works in progress, only one of
| which has been even posted as a preprint so far.
|
| But in general it's reasonably common for a proof to have
| been written up to the best of the author's ability, and for
| it still to be impossible for anyone else to understand it
| well enough to be confident in its correctness.
|
| Formal logic was no help, for two reasons. First of all the
| formal logical systems of the early 20th century were really
| a sort of existence proof, to show that a formal logical
| system can in principle be defined, and were too unwieldy and
| verbose for practical use in non-trivial situations.
| Secondly, it would then become necessary for the reader to
| check the correctness of a proof in formal logic, which is an
| even more difficult task than checking a well-written
| informal proof.
|
| But this is changing: modern formal proof systems are
| designed with user-friendliness in mind, and produce proofs
| that can be verified by computer. It's now starting to happen
| that formalisation can be used as a way out of the impasse
| where a proof is too complicated for anyone but the author to
| understand. I can think of two examples of this: Thomas
| Hales's Flyspeck project [1] was the first such case, and
| required a monumental effort from Hales and his
| collaborators. Much more recently, Randall Holmes's proof
| that NF is consistent was formalised [2], finally putting to
| rest a very old question in the foundations of logic.
|
| 1. https://arxiv.org/abs/1501.02155
|
| 2. https://www.logicmatters.net/2024/04/21/nf-really-is-
| consist...
| 613style wrote:
| Like all writing, proofs have a target audience. If you don't
| know what a Galois group or a modular form is, it's not the
| author's job to teach you.
|
| Formal verification is getting more mainstream, but it's not
| there yet.
| guyomes wrote:
| Expressing proofs as formal logic is a great tool to make
| them more rigorous. Formal proofs are easier to check with a
| computer, provided that all the cases have been fleshed out,
| and that it has been written in a proof-assistant language.
| However those proofs are tedious to write, and a human reader
| has a limited capacity for handling high number of cases.
| Omitting cases and writing out informally why those cases can
| be omitted is crucial to help the reader to follow the proof.
| That is a step where errors can arise.
|
| An example of wrong proof due to sketching quickly some cases
| is the proof that all triangles are isosceles [1].
|
| Here is also an example of an apparently obvious result with
| a non-trivial proof, were all the cases are written out
| formally in the proof-assistant language Coq [2]. It is the
| proof that if we compute the multiplications and the square
| roots with floating-point arithmetic in base 2, then
| sqrt(a*a) is actually |a|. This was assumed without proof in
| some previous papers, and it is easy to understand how the
| authors may have missed it. Note that this result is not true
| in base 10.
|
| Finally, sometimes non-formal proof can actually be more
| convincing than formal proof. For example, it was proven
| formally in 1957 that it is possible to turn a sphere inside
| out continuously, without cutting it, tearing it or creating
| any crease [3]. With more work, this result was later proven
| with a video. The video proof is arguably easier to follow
| and more convincing for a human. The formal proof has not yet
| been formally checked by a proof assistant, although work in
| this direction is on the way [4].
|
| [1]: https://www.themathdoctors.org/false-proofs-geometry/
|
| [2]: https://inria.hal.science/hal-01148409v1/document
|
| [3]: https://en.wikipedia.org/wiki/Sphere_eversion
|
| [4]: https://leanprover-community.github.io/sphere-eversion
| esafak wrote:
| It takes time for reviewers to verify the proofs. The
| correctness may not be apparent. Here's a famous recent case:
| https://en.wikipedia.org/wiki/Inter-
| universal_Teichm%C3%BCll...
| ForOldHack wrote:
| Thank you for clearing this up: A book I was reading attributed
| this to Andrew Weils, where it was Andre Weil, and later in the
| book it discussed Andrew Weils, who was really Sir Andrew Wiles -
| who benefited greatly from the contributions of Andre Weil. Let
| us keep our w(e)iles straight.
| zyklu5 wrote:
| There's another Weyl. Hermann Weyl. A mathematician almost as
| great as Hilbert. In fact he is the person who rigorously
| introduced Riemann surfaces. He is also the originator of Gauge
| theory -- so fundamental to modern physics.
| jl2718 wrote:
| This is not my field, and from loose understanding, so I'll type
| out a hot take off the top of my head and prepare to be corrected
| about it, but... some of the things in the article seemed a bit
| in need of clarification and relevance. Hope I get it right.
|
| Weil is most often encountered in the field of elliptic curves,
| which they alluded to by the form of the polynomial, but they are
| mixing the reference to two types of polynomials. The equivalence
| of finite fields and polynomials was already established by
| Galois, and is maybe the central theory of abstract algebra. Weil
| connected this to algebraic geometry through 'torsion points' on
| an elliptic curve, which is a specific form of polynomial itself
| defined on a (finite) field, that have degree (adding a point to
| itself until it equals itself again) equal to a prime power in
| elliptic algebra (addition is the inverse of the intersection of
| a secant defined by the two points with the curve). This defines
| a group of prime order, and to get a field, he defined a
| 'pairing' function that works like multiplication between two
| group elements and returns an element in an 'extended' curve that
| belongs to a group of the same order and has the same coefficient
| as if the two original group coefficients were multiplied, which
| is known as the bilinearity property. The extension here is I
| think what they mean by 'complex' in that it doubles the degree
| of the field polynomial, which gives a Cartesian product of
| groups from the original definition, and this can be used to
| divide through 'torsion points' back to the field element that
| defines the product point. This opens up an elliptic form of the
| zeta function, which was used to prove the Riemann hypothesis on
| elliptic curves, although not yet extended to the integers, and
| Fermat's last theorem. The most common use of this is probably
| pairing-based cryptography, which is based on bilinearity and
| computational asymmetry of the pairing operation, which is to say
| that you can 'multiply' through the pairing operation, but you
| cannot efficiently factor.
|
| So now you have some context of why it's relevant and some basic
| terms to look up and you'll probably find a lot more precise but
| convoluted language about these things to correct me on.
| Jun8 wrote:
| Totally tangent: One of my favorite nitpicks (some others are use
| of two spaces before a period, the Oxford comma, and the idea
| that light slows down in a medium) is that the Rosetta Stone is
| not trilingual: the two texts is Ancient Egyptian use different
| characters - Hieroglyphs and Demotic. The former is a stilted
| form mimicking Middle Egyptian while the latter would be
| accessible to more people.
|
| So the two are not word for word same but are not different
| languages either.
|
| For a true trilingual inscription that also helped with
| decipherment, see
| https://en.m.wikipedia.org/wiki/Behistun_Inscription
___________________________________________________________________
(page generated 2024-05-07 23:01 UTC)