[HN Gopher] Formalising Mathematics: An Introduction
___________________________________________________________________
Formalising Mathematics: An Introduction
Author : panic
Score : 139 points
Date : 2021-02-21 16:19 UTC (6 hours ago)
(HTM) web link (xenaproject.wordpress.com)
(TXT) w3m dump (xenaproject.wordpress.com)
| adamnemecek wrote:
| I wish these attempts were using constructive mathematics but I
| understand that that would turn away a lot of mathematicians.
| zozbot234 wrote:
| AIUI, the Lean system does support constructive mathematics.
| You can add axioms and reasoning principles that make the
| system non-constructive, but they're entirely optional.
| IngoBlechschmid wrote:
| Yes, you are quite right, but the community around Lean's
| standard library heavily focuses on classical mathematics.
| JadeNB wrote:
| Just pick a different one! There are definitely formalisation
| efforts out there that use constructive mathematics; for
| example Coq is so called after the logic, the calculus of
| constructions, that it uses
| (https://en.wikipedia.org/wiki/Calculus_of_constructions).
| kevinbuzzard wrote:
| Hi! Yes! Just pick a different one! The problem is that
| constructivists have been formalising mathematics for decades
| and have not really managed to break through into the
| mainstream mathematical community with their efforts. The
| difference with Lean's maths library is that we absolutely
| reject constructivism, which makes Lean far less suitable for
| certain kinds of computations but conversely far far better
| equipped for proving all the theorems in an undergraduate
| mathematics curriculum and then going on to tackle research
| level mathematical questions of the kind which most
| mathematicians recognise as "normal mathematics". My argument
| (I should say that I am the author of the blog post) is that
| this resolutely non-classical approach is far more likely to
| arouse the interest of mainstream mathematicians, who
| rejected constructivism 100 years ago and have never looked
| back. I can certainly see a role for constructive
| mathematics, however I know from experience that most working
| mathematicians reject it and hence the pragmatic approach is
| to reject it when formalising if we are to start appealing to
| the mathematical masses.
| Abhinav2000 wrote:
| Dear Kevin,
|
| I am working on some hobby projects, similar but very much
| more elementary to what you are doing. May I please kindly
| get your e-mail address (or you may drop me a note at ashok
| dot khanna at hotmail dot com). I would love to connect and
| follow your work.
|
| I apologise as I was not able to find your e-mail address
| on your blog post - sorry if I missed it.
|
| Best wishes,
| vcdimension wrote:
| AFAIK the advantage of constructivism is algorithms. Coq
| allows you to extract lisp/ML/Haskell programs. Perhaps we
| will be seeing the next generation of fully homomorphic
| encryption programs, or topological data analysis programs,
| automatically generated by Coq.
| auggierose wrote:
| So what about an algorithm you verified in a non-
| constructive way?
| vcdimension wrote:
| You still need to construct the algorithm in the first
| place, which is what a constructive proof does.
| auggierose wrote:
| Sure, but you would not need to prove it in a
| constructive way.
|
| See, that is one of the problems with constructive
| mathematics. It not only requires you to write down the
| algorithm, but also to prove it constructively, although
| a non-constructive proof would be perfectly fine. In
| other words: constructivism is often overkill.
| creata wrote:
| But everything you'd typically see in an algorithm has
| decidable equality, so proofs by contradiction are
| constructively justified, no?
| auggierose wrote:
| I don't know! But I don't think so. Also think about
| other properties of an algorithm, like runtime, etc. You
| could have a non-constructive proof for the upper bound
| on the runtime, but not a constructive one.
| auggierose wrote:
| Here is an example: after inputing positive integers a, b
| and c, output all natural numbers n for which a^n + b^n =
| c^n.
|
| My algorithm: If a + b == c then output 1. If a^2 + b^2
| == c^2 then output 2. Stop.
|
| This algorithm is correct, because Fermat's last theorem
| holds. Now, try to come up with a simpler algorithm than
| that, and one that in addition has a constructive proof.
| [deleted]
| vcdimension wrote:
| I think we're at cross-purposes; I am talking about
| mathematics for the purpose of real-life useful
| applications (e.g. cryptography, data analysis, etc), in
| which case you need algorithms.
| auggierose wrote:
| Nope, we are not at cross-purposes. You just don't
| understand what I am saying.
|
| Let's say you need an algorithm for a real-life
| situation, and you manage to write one down.
|
| Ok then, you are good to go, just use it!
|
| But ... how do you know that the algorithm you have
| written down is correct?
|
| Now, a constructive mathematician would require you to
| also provide a constructive proof for your algorithm. A
| mainstream mathematician would additionally also be fine
| with a non-constructive proof for your algorithm. So, who
| is more real-life?
| vcdimension wrote:
| Yes, but if I told IBM that I had a proof that a
| particular algebraic property or relationship related to
| homomorphic encryption holds true, I'm sure they would
| much prefer that it was constructive, rather than non-
| constructive, because they can produce a usable algorithm
| from the constructive proof. The point is that by
| exploring mathematics using only constructive proofs, we
| are guaranteed to produce (possibly useful) algorithms.
| If you already have an algorithm, and can prove it works
| non-constructively then fine, but a collection of N non-
| constructive proofs is not nearly so useful for real-life
| applications as a collection of N constructive ones.
| auggierose wrote:
| Your argument is wrong in so many ways, but let me just
| show you one: A constructive proof guarantees that there
| is an algorithm, but it doesn't say anything about the
| runtime of that extracted algorithm. Now, what good is an
| algorithm that is much too slow to be practically useful?
|
| In general, my hypothesis is that if you restrict
| yourself to constructive mathematics, you are limiting
| yourself. And that is true whether your chosen field is
| algorithms, or not.
|
| Now, if you offer me for a given algorithm a constructive
| proof, that's great. But if you needed 10 years to give
| me that proof, and a non-constructive one can be had in
| 10 minutes, I might not be so enthusiastic if I had to
| pay your salary, or if I needed that result really
| urgently, or both. But on the other hand, IBM probably
| doesn't care.
| vcdimension wrote:
| Hey, there's no need to by so impolite. My argument is
| not wrong, it's just a different argument to yours (which
| I fully understand, and is not difficult to grasp). Your
| example doesn't discount mine in any way; a slow
| algorithm is still better than no algorithm at all. The
| point about proving the correctness of an existing
| algorithm is moot, I'm talking about mathematical proofs
| which in themselve lead to algorithms. I'm not claiming
| we should abandon non-constructive mathematics, just that
| formalizing mathematics constructively leads to more
| useful algorithms. Similar to the argument that some
| programmers make about constraining themselves to think
| purely functionally in order to produce less buggy code.
| Goodnight.
| [deleted]
| guerrilla wrote:
| The Four Colour Theorem in Coq seems pretty mainstream I'd
| say... Also I guess you know that you don't personally have
| to reject LEM to use Agda or whatever, you just can't do
| everything in it or at least everything the classical way.
| kevinbuzzard wrote:
| This is a milestone result, and its formalisation taught
| us many things, for example that the systems are capable
| of handling long proofs about elementary objects.
|
| However finite graph theory is not _remotely_ mainstream
| mathematics. Take your favourite super-prestigious maths
| prize, for example the Abel Prize or the Fields Medal.
| Now look at everyone who has won this prize in the last
| 10 years. That is the definition of mainstream
| mathematics. And as you will see if you do this, the
| areas which these people are working on are a million
| miles away from finite graph theory. This is _precisely
| the problem_. Computer scientists sometimes have a very
| twisted view of exactly what kind of mathematics is
| regarded as _important_ in 2021. The experiment I outline
| above will give you some idea of what is mainstream, and
| believe me, it 's not the four colour theorem.
| kmill wrote:
| I suppose it's not exactly mainstream, but Kronheimer and
| Mrowka are among those trying to prove the four color
| theorem using instanton homology and gauge theory. It's
| certainly not finite graph theory, though (their idea of
| a 3-regular graph is the singular locus of a certain kind
| of orbifold!)
| QuesnayJr wrote:
| Finite graph theory is completely mainstream mathematics.
| There's a kind of elite provicialism that you sometimes
| see, where only the mathematics that's done at Harvard or
| wins the big prizes counts, and this is a good example.
| There are probably more people employed in math
| departments working on finite graph theory than there are
| working on the Langlands Program. Robertson and Seymour
| were too old to be eligible, but the fact that someone
| like them could never win the Fields Medal, while someone
| in other fields could, is a statement about who is well-
| connected with the prize committee, and not a general
| statement about mathematics.
|
| And I say this as someone with no interest in graph
| theory, or combinatorics in general.
| spekcular wrote:
| Buzzard's post suggests to me that when he says
| "mainstream," he means what the community at large thinks
| of as important and field-defining (cf. the sentence with
| _important_ in it). He is totally correct here; in this
| sense finite graph theory is not mainstream mathematics.
|
| Further, I don't think it is "elite provincialism" to
| point out this readily verifiable fact. Besides looking
| at the big prizes, we can look at any of the top journals
| (Annals, IHES, Inventiones, Journal of the AMS, Acta,
| whatever). You're not going to find a lot of finite graph
| theory there.
|
| Now, I think we should separate the question whether it
| _is_ the case that he 's right about what mathematicians
| value from the question of whether it _ought to be_ the
| case that the world is this way. As I just said, the
| answer to the first question is _yes_. I 'd argue that
| the answer to the second question is also _yes_ , but
| that's a whole different discussion.
| QuesnayJr wrote:
| Pointing to the top journals is again a statement about
| who is well-connected, so if anything it is further proof
| of my claim of elite provincialism. Mathematics has
| politics, like any other field, and it's politics that
| determine that the proof of the Robertson-Seymour Theorem
| appeared in the "Journal of Combinatorial Theory" and not
| JAMS.
|
| The irony is that I suspect every single mathematician,
| elite or not, knows what the four-color theorem is, far
| more than could tell you what chromatic homotopy is, or
| state anything about the Langlands program beyond "Uh,
| it's something about number theory? And groups? Maybe?"
| spekcular wrote:
| I think the (implicit) charge that the editors of top
| journals are keeping good papers out for snobbish reasons
| is mostly unfounded. I don't deny that their tastes shape
| what gets published, of course. But in most
| circumstances, they are not subject matter experts, and
| the first step of evaluating any paper is that is not an
| obvious desk-reject (for poor writing, crankery, etc.) is
| to send it to a group of relevant experts for "quick
| opinions." Only if these opinions are sufficiently
| positive is the paper sent for a full referee report
| (again by an expert), and in most (but not all) cases the
| referee's suggestion is followed. So the picture of
| editors just arbitrarily killing papers they don't like
| is not accurate.
|
| Further, it's not like _no_ finite combinatorics /graph
| theory gets published in these journals. Just not a lot,
| because it's not sufficiently interesting/valuable to the
| broader community. (Annals of Math almost published
| Hales's proof of the Kepler conjecture, after all;
| eventually a proof appeared in another top journal.)
|
| Also, re: connections, you can easily check the author
| affiliations for papers in these journals. There are
| plenty of people from universities that are not so well
| known. It's hardly an "old boys club."
| QuesnayJr wrote:
| There was a notorious case that a paper by Wehring
| solving the largest outstanding question in lattice
| theory was rejected by JAMS despite glowing referee
| reports (and being pretty short). So it's pretty much an
| example of editors arbitrarily killing a paper. (It
| appeared in Advances in Mathematics.)
|
| You can see a letter to the editor of the Bulletin about
| it. Look at the affiliations of the people protesting the
| decision, and the affiliations of the editors defending
| it: http://www.ams.org/notices/200706/tx070600694p.pdf
| spekcular wrote:
| I don't really see a problem with this decision, though I
| am sympathetic to Wehrung. As the editors note, there are
| a ton of great papers JAMS doesn't publish (due to severe
| page count constraints at the journal). Their reasoning
| is not "arbitrary"; it was spelled out quite clearly for
| the authors in the rejection notice they got. Many other
| papers in "trendy" subjects face the same fate.
| QuesnayJr wrote:
| What do you think they say? "You're not well-connected,
| so we're rejecting you"? How do you think political
| decisions get defended in academia? For insiders, you
| listen to the referees. For outsiders, you invoke some
| vague criterion of lack of fit or lack of interest. And
| people can come along and say "If this field is
| important, why doesn't it appear in JAMS"? It's a self-
| fulfilling prophecy.
| spekcular wrote:
| You seem determined to believe that the rejection was for
| "political" reasons despite having no evidence for this
| claim. The quoted reasoning was not "lack of fit" or
| "lack of interest," it was lack of "interaction with
| other areas of mathematics." Going back to my first
| comment, there's a general sense in the community that
| this sort of interaction among mathematical subfields (or
| with physics) is prized in research, and it's one of a
| few criteria that form the sociologically dominant view
| of what constitutes "good mathematics." You might
| disagree with these criteria, but it's not hard to see
| why that paper might lose out to other excellent papers
| when judged by them. This doesn't look like politics
| (favoring "insiders") to me; it looks like the consistent
| application of a value judgment about what good research
| is.
|
| Again, whether you think the criteria should be the way
| they are is a separate conversation.
| JadeNB wrote:
| > resolutely non-classical approach
|
| Calling this 'non-classical' is interesting--it's
| definitely non-classical from the point of view of
| formalisation, but I'm not sure formalisation has been
| around long enough to have classics ....
|
| As of course you know but non-mathematicians may not, from
| a non-formalising mathematician's point of view, it's the
| non-constructive logic that's classical, to the extent that
| it's actually sometimes called classical logic
| (https://en.wikipedia.org/wiki/Classical_logic).
| kevinbuzzard wrote:
| :-) Yes, by assuming classical logic the Lean community
| is taking a non-classical approach to bringing
| formalisation to the masses :-)
| Abhinav2000 wrote:
| What is constructive mathematics for the layman?
| a1369209993 wrote:
| Roughly, that proving a statement of the form "For all
| a,b,c,..., there exists x,y,z such that some statement
| involving a,b,c,...,x,y, and z is true." requires actually
| _constructing_ suitable x,y, and z given suitable a,b,c, etc
| to derive them from.
| zozbot234 wrote:
| With the proviso that the non-constructive statement '[?] x
| such that P(x)' can also be understood constructively as
| '![?] x !P(x)' which does not require constructing a
| suitable x, so classical proofs _can_ be modeled without
| adding any extra axioms to the logic. (Clearly the two
| statements are classically, though not constructively
| equivalent).
|
| Similarly, all classical uses of LEM (A [?] B) can be
| understood as constructive statements of the form !(!A [?]
| !B).
| Abhinav2000 wrote:
| Thanks
| ithinkso wrote:
| Constructive mathematics rejects the law of excluded middle.
|
| In a non-constructive mathematics it is true that 'either A
| or not A is true' and that allows you to prove existence of
| objects with certain properties by disproving their non-
| existence (if it cannot not-exist then it has to exist, by
| the law of excluded middle). Constructive mathematics, on the
| other hand, says that that's not enough and to prove that
| there exist objects with some properties you have to prove
| their existence.
| abhinav22 wrote:
| Thanks
| stacksemantics wrote:
| Constructive mathematics does not affirm excluded middle.
| That's distinct from rejecting it.
| kevinbuzzard wrote:
| It's mathematics where certain kinds of proof by
| contradiction are not allowed -- if you want to prove that
| something exists because you want to use it, then you have to
| make it, you can't just say "let's assume it didn't exist and
| go on from there to deduce that 0 = 1 which is definitely
| wrong, so our assumption is wrong, so it exists, so let's use
| it".
|
| Here is the reason why it's obvious for mathematicians. If
| you're trying to prove a theorem (e.g. the theorem that class
| numbers of imaginary quadratic fields tend to infinity), and
| then someone comes up with a proof which assumes that a
| certain generalisation of the Riemann hypothesis is true, and
| then someone else comes up with a proof which assumes that
| the exact same generalisation is false, then we
| mathematicians say "great, the theorem is now proved". This
| actually happened.
|
| However if your boss asks you to write some code which does a
| calculation, and the next day you show up in their office
| with two USB sticks and say "this code is guaranteed to
| produce the correct answer if the Riemann hypothesis is true,
| and this other code is guaranteed to produce the correct
| answer if the Riemann hypothesis is false" then you are going
| to lose your job, because all you did was prove that the code
| exists, which is less helpful than it could be.
|
| For me one of the biggest problems with the area of
| formalisation of mathematics is that for decades it has been
| dominated by computer scientists, whose view of what is
| important and beautiful in mathematics does not really
| coincide with that of the working mathematician. This is what
| I am fighting to change.
| vmilner wrote:
| I remember when encountering my first (or one of my first)
| proof by contradiction (irrationality of sqrt(2), say)
| feeling unsatisfied because I didn't know how one could
| know that it was _your_ assumption that was wrong and not
| one of the more fundamental ones of mathematics.
| auggierose wrote:
| > This actually happened
|
| Oh wow! Was it an interesting theorem that got proved this
| way? Did it get proved in another, less controversial
| manner as well? Could you provide a pointer to it?
| Someone wrote:
| https://en.wikipedia.org/wiki/Riemann_hypothesis#Excluded
| _mi... lists 3 such proofs.
| auggierose wrote:
| I'd say it is still a pretty constructive answer, as you
| can run both codes, get two concrete answers, and one of
| them is guaranteed to be right.
| kmill wrote:
| A way to think about whether something is constructive is
| that everything is decidable, in the sense that there is
| some procedure that will give you the answer in finite
| time.
|
| In Kevin's example where you have two programs, one which
| depends on the Riemann hypothesis being true and the
| other which depends on it being false, is that you can't
| just execute the programs -- they might have undefined
| behavior since they depend on the truth of some statement
| during their executions, and there's no general algorithm
| to decide whether undefined behavior is happening. They
| depend on undecided facts, so you can't put them together
| into a single program that decides the result. (Maybe a
| slogan is "truth can be contingent, but data cannot be.")
|
| In Lean syntax, this is an example type signature of
| something that takes two programs (h and h') that
| respectively take in the truth/proof of a proposition or
| its negation, along with a proof that there is at most
| one element of a, and produces that element. I don't
| think there's a way to write this definition in Lean
| without marking the definition noncomputable:
| def extract {p : Prop} {a : Type*} (h : p - a)
| (h' : !p - a) (unique : [?] (x y : a), x = y) : a
| := sorry
|
| (the sorry indicates a missing definition).
| auggierose wrote:
| Yeah, I really was joking.
| Abhinav2000 wrote:
| Thanks Kevin. It seems like having both approaches is more
| flexible and thus more general (which can hopefully only be
| a good thing?). One could always replace a proof by
| contradiction later with a direct proof, but there's
| definitely value in using it in the meantime (at least in
| my uneducated view).
|
| p.s. could you let me know your e-mail so I can keep for
| future reference, as I'm also working on a hobby project
| for automated theorem solving.
| sgeisenh wrote:
| https://en.wikipedia.org/wiki/Intuitionistic_logic
|
| If you are familiar with "Classical" logic, constructive math
| omits the law of excluded middle (e.g. "A or not A" must be
| true). In ZFC, the axiom of choice is omitted.
|
| This leads to proofs that are not only a verification of some
| idea but also gives you the mechanism to compute the
| evidence. This is often described as "the computational
| content of proofs" and is especially valuable in the context
| of the Curry-Howard isomorphism: for every proof, there is a
| corresponding program (and vice-versa). This is the basis for
| formal verification of constructive proofs. When creating a
| proof in Coq, you are actually writing the corresponding
| program. And you can even extract the program in another
| general purpose programming language (usually OCaml in the
| context of Coq, but Haskell is also supported).
| [deleted]
| abhinav22 wrote:
| Many thanks
| rssoconnor wrote:
| A lot of responses are going to say something like "it is
| mathematics without using the law of the excluded middle, or
| proof by contradiction" or something like that. They are not
| technically wrong, but I'd like to offer a different
| perspective.
|
| The constructive logic used in constructive mathematics is
| classical logic with two new connectives _added_ : the
| constructive existential, and the constructive disjunction
| (which could be defined in terms of the constructive
| existential).
|
| The constructive disjunction and constructive existential
| connective has semantics given by the BKH interpretation[1].
| A proof of the constructive disjunction A + B is either a
| proof of A or a proof of B. A proof of the constructive
| existential Sn:N. P(n) is a pair <n,p> where n is a natural
| number and p is a proof of P(n).
|
| So constructive mathematics isn't classical mathematics
| hindered, but constructive mathematics is mathematics
| enhanced with a _more expressive language_. Naturally
| constructive mathematics tends to focus on theorems written
| in this more expressive language that make use of these new
| constructive connectives, rather than focusing on the
| classical fragment which is already well studied.
|
| For the non-layman: we can see that the above interpretation
| is correct because the fundamental logical rules for
| universal quantification, implication, conjunction, false and
| true are all identical between classical and constructive
| logic. And, according to classical mathematicians at least,
| this set of logical combinatorics is complete. Thus the law
| of excluded middle holds, even in constructive logic, so long
| as you use the classical disjunction, which is defined in
| terms of conjunction, implication, and false. Similarly you
| can prove that proof by contraction, i.e. double negation
| elimination ! !A -> A is a theorem of constructive logic
| whenever A is a formula that does not use the constructive
| disjunction or constructive existential (where negation is
| defined in terms of implication and false).
|
| For the all of the above, I'm particularly focused on first-
| order number theory, however all of the above carries over to
| higher-order theories, and I think it even holds for set
| theory (or at least some large part of set theory such as
| Zermelo set theory; I forget what happens with the
| replacement axiom). Higher-order constructive mathematics
| does come with the caveat that the Axiom of Choice is not a
| theorem of constructive mathematics even when it is phrased
| only using the classical existential.
|
| [1]https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%8
| 0%...
| abhinav22 wrote:
| Thanks!
| guerrilla wrote:
| Most are... like Coq, Agda, HoTT, etc.
| cjfd wrote:
| There does not seem to be any reason for mathematicians to be
| turned about by these engines using constructive mathematics.
| One can use excluded middle as an axiom and do all the
| classical mathematics one likes. What becomes much easier if
| the engine is constructive is telling which theorems depend on
| excluded middle and which do not.
| zozbot234 wrote:
| This is in fact how Lean works - the basic logic is
| constructive and excluded middle is an "extra" axiom. But
| even that is not as elegant as just writing non-constructive
| statements in the negative fragment of the logic, where
| (AIUI) one can already reason classically with no need for
| extra axioms.
| kmill wrote:
| I know we've discussed on HN before whether the elegance of
| the negative fragment extends to practice, but something
| about Lean is that it doesn't have LEM as an axiom. It's a
| theorem following from (a version of) the axiom of choice,
| the existence of quotient types, proof irrelevance (proofs
| of the same theorem are equal), and proposition
| extensionality (logically equivalent propositions are
| equal). Lean doesn't let you construct things that
| materially depend on LEM however -- you can only use it to
| prove that already constructed things have desired
| properties.
| enricozb wrote:
| In case anyone is curious, the proof of LEM from AC is:
| Diaconescu's Theorem [0]
|
| [0]: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
| #:~:text....
| kmill wrote:
| After working with Lean for a while, I've started to appreciate
| that there is a wider range of what it means to be constructive
| -- being "fully constructive" seems to me to be like fanatical
| efforts to make everything X, for example "everything is a
| function" or "everything is an object" and so on.
|
| In the Lean approach, anything not marked `noncomputable` in
| the Type universe and above needs to be constructible, in the
| sense that there is a program that can compute such an object
| using a functional programming language (where the function is
| guaranteed to terminate), but proofs don't need to be
| constructible in the same way. Proofs are still functions, but
| they're free to use things like the axiom of choice in the
| course of a proof. The way things are set up, even if you use
| non-computable things while making your inferences, this
| "forbidden" data will not leak out.
|
| It seems eminently reasonable to me that you can argue a
| program computes the correct thing because it doesn't compute
| the wrong thing, and unless you're specifically studying
| different toposes/logics, I'm not sure what constructive logic
| would really give you (and it's not like mathematicians
| slavishly keep track of where they used the axiom of choice or
| its consequence the LEM).
|
| How this all looks in Lean practice is that it's stronger to
| give a definition and prove it satisfies a property than to
| prove a "there exists" statement. mathlib authors tend to go
| for the first, unless the result is inherently noncomputable.
| There's also a facility for lifting propositions up to boolean
| values, which more or less amounts to giving a constructive
| proof -- this is used pervasively, for example with finite
| sets, which are constructive in the sense that if you have one
| there's an actual finite list backing it.
|
| I guess in short: it's a useful middle ground being able to
| prove something exists without having to construct it, but if
| you want to "have" the thing that purportedly exists you need
| to construct it.
| breck wrote:
| I will pay $3.14 to the first person that formalizes mathematics
| using only https://treenotation.org/.
| drdeca wrote:
| This appears to just be saying "using python style indentation
| to represent trees"? I don't understand the significance. Like,
| yeah, you can express whatever tree you want that way. Plenty
| of other ways to represent trees. It's a nice enough default if
| you don't know anything about the sort of thing the tree will
| contain.
|
| But there's a reason that when writing conditionals, we don't
| put each symbol in the expression on their own line. Those also
| have their own tree structure, they are also part of the AST,
| but we put many of the nodes on the same line for ease of
| reading and editing.
| breck wrote:
| > But there's a reason that when writing conditionals, we
| don't put one symbol in the expression on their own line
|
| I won't disagree with you. However when you zoom out and
| crunch the numbers, you'll find that although there are
| infinite expressions to put in conditionals, in practice an
| absolutely minuscule amount of those patterns are actually
| used.
|
| Context free grammars are not free.
|
| Better ways are coming.
| RedouaneBrahimi wrote:
| Novak Djokovic Wins Third Straight Australian Open Title
|
| https://snip.ly/8mepd7#https://www.nytimes.com/2021/02/21/sp...
| JadeNB wrote:
| Wrong thread?
| mckirk wrote:
| No, it's probably just a good idea to remind people of this
| feat, similarly to the legendary wrestling match in nineteen
| ninety-eight when The Undertaker threw Mankind off Hell In A
| Cell and plummeted 16 ft through an announcer's table.
| schoen wrote:
| A game to try this out (by Kevin Buzzard, who is participating in
| this thread and is also the author of this blog post).
|
| https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
|
| I loved it and have been trying to make some subsequent levels
| about divisibility.
| uyt wrote:
| I played it recently. I spent almost a full day to finish all
| the worlds and then lost interest afterwards.
|
| I think I had expectations that it would be a lot less ...
| tedious? Like I was hoping it would be mostly automated except
| needing hints whenever it got stuck. Much like how the flavor
| text would hint to you (the human) that you needed to use
| certain theorems for certain levels.
|
| Instead, it was so low level that you had to do every step of
| algebra manually with a line of code each. (and to be fair, in
| the beginning it was necessary because you're developing the
| usual rules of algebra as you go, but even in the later levels
| after they tell you about the ring tactic there's still a lot
| of manual algebra you need to do) The search space seems small
| enough that even I was just mindlessly spamming
| rewrite/intro/apply/induction. Why can't a computer automate
| this completely.
|
| And going in the other direction, I was hoping this would be a
| good tool to aid in proofwriting. But most of the "proof" I
| wrote was complete gibberish not meant for human consumption. I
| think the problem is because the code relies heavily on
| mutating a context that you can't see without using the lean
| UI.
|
| Anyway, maybe the number game is just not a good intro to the
| full capabilities of lean and I am missing the point.
| ahelwer wrote:
| No, I think you have a pretty good grasp of things. In the
| real world people do use more powerful tactics like ring to
| skip all the low-level algebraic manipulation (which I
| personally really enjoyed but can see others finding
| tedious).
|
| Your point about proof readability applies to interactive
| theorem provers generally. You can see a tradeoff here
| between Lean/Coq and more "literate" formal proof languages
| like TLA+, which has a prover called TLAPS (TLA+ Proof
| System). TLA+ proofs are written in a hierarchical style
| Lamport proposed in his paper _How to Write a 21st Century
| Proof_ [0], and are readable by themselves. The BIG BIG
| tradeoff here is that when you're writing the proof in TLA+,
| it's very difficult to know what the prover is "thinking" and
| why it is stuck. Whereas with interactive provers you know
| exactly what the prover is "thinking" - the proof consists
| solely of instructions to manipulate those thoughts which you
| see on screen at all times! So at this time it seems there's
| a tradeoff between ease of writing a formal proof and ease of
| reading a formal proof.
|
| [0] https://www.microsoft.com/en-
| us/research/publication/write-2...
| bsdz wrote:
| Last month Kevin Buzzard gave an interesting talk "How do you
| convince mathematicians a theory prover is worth their time?"
| about how he became involved with LEAN and some of the proofs he
| formalised with it:
|
| https://youtu.be/8PLrxAfmC_o
| zant wrote:
| I absolutely love everything about this. Specially how it can
| provide access to knowledge to people all around the world.
|
| I'm currently thinking about getting a degree in Maths, and I
| find extremely appealing the notion of having a repo of knowledge
| from where to gather theorems, specially useful for newer
| developed areas.
| carapace wrote:
| The only major problem (IMO) is that Lean and the others (Coq,
| Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read.
|
| Check out "Automated Propositional Sequent Proofs in Your Browser
| with Tau Prolog" for a promising approach:
| https://www.philipzucker.com/javascript-automated-proving/ It's
| rendering LaTeX proof trees.
| asdftemp wrote:
| that is a neat demo with a lot of useful links! In fact, it
| seems that the Lean developers/community are very interested in
| new methods of achieving readability, and providing users with
| tools to build interfaces that scale up to the complexity of
| real workflows.
|
| For example, Lean in vscode supports interactive html
| "widgets": https://youtu.be/8NUBQEZYuis?t=453
|
| (at that timestamp, there's a quick introduction to their
| typical use at the moment).
|
| lean4 is committed to all sorts of extensibility; here's a
| demonstration of the new macros:
| https://twitter.com/derKha/status/1354082976456441861. There
| have also been several instances of users implementing old
| lean3 features (for example, the `calc` tactic mode, which has
| unique syntax for proving (in)equalities) by simply defining
| new type classes and short macros.
| nynox wrote:
| Following this proof tree idea, this recent paper
| https://arxiv.org/abs/2102.03044 suggests to think of proofs of
| theorems as large trees, a tiny subset of which needs to be
| made explicit to convey the confidence the rest could be
| written out (if ever needed).
| fjfaase wrote:
| I think that something like http://us.metamath.org/index.html has
| already gone a long way in formalizing math. And this is not the
| only attempt to formalize math, but it is unique that it uses a
| very limited amount of syntax and rules, and makes use of a
| simple (small) proof engine, which makes verifying that the proof
| engine is correct possible.
| JadeNB wrote:
| A small proof engine, and maybe a limited amount of rules
| (depending on the exact technical meaning of 'rules') is a good
| thing, but I'd say a limited amount of syntax is a bad thing.
| Mathematicians as a community tend to be happy with--I might
| even say to prefer--lots of syntax, and, if you want to get a
| formalisation process really going, layering it with enough
| syntactic sugar to bring in mathematicians who aren't usually
| 'formalisers' is going to be essential.
|
| It's also true that there are lots of attempts at formalisation
| out there; I happen to know about vdash.org , for example, but
| there are certainly others. I think it's _good_ to have an
| abundance of formalisations, since no one formalisation style
| is going to appeal to everyone (for example, as already
| discussed above, probably the more formalisation-minded
| mathematicians will have a higher tolerance for minimalism).
| Gehinnn wrote:
| Lean allows for third party type checkers. There are relatively
| small alternative type checkers for Lean (e.g. a scala
| implementation [1]).
|
| Lean's power lies in its elaborator that breaks down complex
| tactic-based proofs to a core proof language. This elaboration
| process can be extended with custom tactics and custom syntax,
| making it way more powerful than metamath.
|
| [1]
| https://github.com/gebner/trepplein/tree/master/src/main/sca...
| kevinbuzzard wrote:
| The problem with metamath is that you basically have to be a
| fully signed-up masochist in order to do anything nontrivial
| with it. People have certainly done nontrivial things with it
| e.g Carneiro and the prime number theorem -- but it takes all
| sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 +
| 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving
| that from the axioms of a ring directly in metamath, I
| challenge you to do it in fewer than 30 moves. I should also
| say that whilst Metamath has certainly formalised a whole bunch
| of mathematics, it has not _remotely_ gone "a long way" by any
| reasonable measure which a mathematician would use. For
| example, how much of an undergraduate mathematics curriculum
| does it have? How much representation theory? None. How much
| differential geometry? None. How much commutative algebra?
| Epsilon. These are the measures which mathematicians use, not
| lines of code. It is time that formalisation started to appeal
| to mathematicians, and for this to happen it is essential that
| it starts to demonstrate that it can actually do a _lot_ of the
| kind of mathematics which is recognised as "completely
| standard undergraduate material and hence trivial" by
| mathematicians. It is still the case that these systems cannot
| do certain things which were known to Gauss or Euler (for
| example it was only this year that Lean learnt the proof that
| the class group of an imaginary quadratic field was finite, and
| as far as I know no other system at all has class groups -- but
| we teach this to the undergraduates!). Just saying "large code
| base therefore we've gone a long way" is not the correct logic.
| The question is how much of it is recognisable as worth
| teaching to undergraduates in 2021, and conversely how much
| stuff worth teaching to undergraduates in 2021 is _not_ in any
| of these systems. That's where the problems begin to show up.
| In Lean we are well into a project of formalising an entire
| undergraduate curriculum and within about two years we will
| have finished.
| dwheeler wrote:
| > The problem with metamath is that you basically have to be
| a fully signed-up masochist in order to do anything
| nontrivial with it. People have certainly done nontrivial
| things with it e.g Carneiro and the prime number theorem --
| but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)=
| a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good
| luck proving that from the axioms of a ring directly in
| metamath, I challenge you to do it in fewer than 30 moves.
|
| While it's _allowed_ , generally Metamath users do not prove
| constructs directly from axioms, for exactly the same reason
| as you don't do it in Lean or traditional informal
| mathematics. You're right that most Metamath tools have fewer
| automated tactics, but there _are_ tools with some
| automation, and people are working to improve that.
| dash2 wrote:
| Outsider's question: is it likely that projects like Lean and Coq
| will ever feed into stuff that applied researchers find useful?
| By applied researchers I don't mean "applied mathematicians" but
| scientists who use maths in their field.
|
| As an economist, I sometimes want to prove things that a real
| mathematician could do in their sleep. There's Mathematica and
| friends, but they have their limitations, i.e. they can do what
| you tell them but can't typically "find their own way" to the
| proof of a theorem. Might these systems ever come down to my
| level?
| huijzer wrote:
| Applied computer science researchers have already used Coq to
| verify certain programs and compilers. So, basically, it has.
|
| I think that I would agree with the author about the
| application of machine learning to this domain. Basically,
| proving means searching for the right pieces in the right order
| in an enormous space. If an machine could guess the right path,
| then proving could be automated much more, and that would be
| useful for applied researchers indeed.
___________________________________________________________________
(page generated 2021-02-21 23:00 UTC)