Karl Palmskog (Jun 08 2020 at 10:42): Karl Palmskog (Jun 08 2020 at 10:42):so it seems Lean+Buzzard is creating some buzz around "number games", which are essentially websites running Lean with some gamification on top, targeted towards beginners, see the interface and the source. Surely jsCoq could be used for something similar?
Donald Sebastian Leung (Jun 08 2020 at 11:51):Speaking of websites with theorem-proving games/exercises, Codewars has quite a few of them in Coq (currently 82). In particular, 6-8 kyu exercises make for good beginner practice material IMO
(Sorry for the shameless advertisement, I couldn't resist XD)
Karl Palmskog (Jun 08 2020 at 12:01):codewars is nice, but IMO the signup is a big barrier
Théo Zimmermann (Jun 08 2020 at 13:08):@Donald Sebastian Leung Codewars is now advertised on the Coq website BTW (https://coq.inria.fr/documentation).
Donald Sebastian Leung (Jun 08 2020 at 13:17):Théo Zimmermann said:
Donald Sebastian Leung Codewars is now advertised on the Coq website BTW (https://coq.inria.fr/documentation).
Thanks for your support!
Karl Palmskog (Jun 08 2020 at 13:25):we also have Codewars listed in Awesome Coq: https://github.com/coq-community/awesome-coq
Kevin Buzzard (Jun 21 2020 at 13:47):There is a constant stream of people (mostly mathematicians) appearing on the Lean chat saying they got interested in theorem provers because of the natural number game. I believe that there is plenty more room in this area. Here are some thoughts about what I learnt when putting this together.
Tactic mode is perfect for mathematicians. Definitions are hard (they are all hidden from the user in the natural number game (NNG)) but simple tactic proofs are found enjoyable, especially the buzz you get when you solve a problem.
To get going with teaching mathematicians, you have to figure out a way to teach about ten basic tactics: in Lean they're called intro, exact, apply, cases, induction, left/right (when the goal is an or), split (when the goal is an and), rewrite, refl, and perhaps one or two more; most of these have similar names in Coq.
At least one mathematician expressed some skepticism with the idea that mathematicians would get excited about a game which develops the naturals from Peano's axioms, because this sort of thing is not done in a typical mathematics degree. But it was something which bubbled to the top when I was experimenting with various ideas and trying to figure out how to teach Lean. Another thing which bubbled to the top was basic manipulation of propositions and sets. I don't say anything about sets in NNG (i.e. functions X -> Prop) but the forthcoming real number game (something I'm hoping will be in some sort of shape by the end of the summer) will start with some set stuff, and then move on to basic analysis. I am pretty sure that there is enough room for a sets/logic game, just doing basic stuff like proving , and I think the audience will be there.
One reason that the natural number game works for some people is because I say essentially nothing about type theory; mathematics departments typically do not teach any type theory, and the set theory language ("a group is a set G equipped with a multiplication operation...") is embedded in the standard undergraduate textbooks and lecture courses.
One thing that struck me about a lot of the literature I read when I was trying to learn about theorem provers was that they are written with computer scientists in mind and have very little of what a mathematics undergraduate recognises as mathematics. This sounds like a stupid issue but in general I think mathematicians find stuff like software foundations hard going, for all the wrong reasons: I think the material should be accessible to them, but things like lists are probably fundamental ideas for any computer scientist, whilst being in some sense "a lot of fuss about nothing" to a mathematician; the specification is trivial, and the implementation is of no interest to us. This makes the entire theory of lists in some sense intrinsically uninteresting. I was amazed when I discovered that proving reverse (reverse L) = L was hard; in contrast, in an undergraduate mathematics degree, essentially the only induction you ever need is strong induction on the naturals. No answers here, just some flags.
AI people have told me that they would be interested in seeing databases where each theorem has many proofs. Saving proofs which compile would be of interest to these people.
If anything comes from this, please feel free to ping me. I would be more than happy to push it on social media, would be happy to host a guest blog post by someone from the Coq community, etc. I am too old to start learning the ins and outs of another theorem prover, but would be more than happy to work with the Coq community.
jco (Jun 21 2020 at 14:33):I probably don't have a lot that is worth cluttering the responses for, as I'm a newcomer to Coq myself coming from a CS (and functional programming) background, but I just want to say that I love your goal, and I think it's super interesting to see the mathematical perspective. I am someone for whom CS always came "more easily" than math...stuff like automata theory, complexity theory, that sort of thing all seemed to resonate much more easily than say...real analysis. But I feel like I've come full circle: now I'm getting into proof assistants (largely with CS-oriented aims), but it is making me want to learn more math. Part of that is pragmatic (to use a proof assistant, you have to do a lot of theorems, and mathematicians do a lot of theorems), but another part of it is just that...I dunno, to me, and I am probably not an outlier among this group but am an outlier among learners, math with a proof assistant is so fun! It can be frustrating when something obvious like reverse(reverse l)=l takes so long (I no joke spent about 20 hours doing that in software foundations, stubbornly not wanting to look up what I was missing and building up a massive (unnecessary, heh) series of proofs when what I really needed was just strong induction!!!!). But like, I remember picking up a book on Algebra and getting to the exercises and it's like...do I even understand what this is asking?! I think I know how to solve it, but is it correct?? With a proof assistant, you know the answer: YES. or, well, NO, as is often the case. So while my goals are more CS oriented, I'm excited to dive more into how these tools are used for more pure math
I will also say that in my time in the FP community the weird interchange regarding "what is useful math" has been interesting (and sometimes contentious?). As you highlighted, a lot of people on the CS side of things are excited by type theory of category theory...which don't even register for a ton of mathematicians.
Alexander Gryzlov (Jun 21 2020 at 14:40):Looking through mathematician's glasses is certainly fun, however I suspect that proof assistants will at some point split into those specialized for CS and those aimed at mathematicians. This is already hinted at in e.g. https://arxiv.org/abs/2003.01491:
We believe that XTT is an ideal language for dependently typed programming, in which it is very important that coercions may be erased prior to execution (a procedure that cannot be applied to coercions arising from the univalence principle). Unfortunately, there are several obstacles rendering both OTT and XTT unsuitable for use as languages for formalizing general mathematics, disadvantages not shared by homotopy type theory or its cubical variants.
Kevin Buzzard (Jun 22 2020 at 00:22):Ooh! Another super-important comment: the natural number game is pretty much computer-only. Any game which ran on a phone would, I believe, have far higher take-up. I think the approach we used in NNG, where some WASM trickery is used to get a javascript copy of Lean running in your browser, is doomed to failure on mobile -- but I am certainly not an expert in these matters.
The reason I think that mathematicians are an important target audience with these games is that for computer scientists, you already won. Type theory courses are normal parts of any CS syllabus (at least as far as I know -- there's certainly at least one at my uni) and theorem provers are sometimes used in these courses, and nobody bats an eyelid -- it's normal. It is vanishingly rare to see a computer proof checker being used in a maths department, the staff don't know about them so the students don't learn about them.
@Alexander Gryzlov If you're right, where will Coq go? It has made some spectacular contributions in both areas. My feeling is that there are still some very basic questions which we don't understand though, when it comes to formalising undergraduate level mathematics. I've not seen a practical working definition of manifold robust enough to be usable to do undergraduate level example sheet questions yet -- in any theorem prover. If nobody can do undergraduate example sheets, no way will the maths researchers take any of these systems seriously.
Théo Zimmermann (Jun 22 2020 at 08:27):On behalf of the Coq developers, I can say that there is a commitment to keep supporting the use cases of the two communities (mathematicians and computer scientists). Coq is and will remain a general purpose theorem prover.
Théo Zimmermann (Jun 22 2020 at 08:30):From what I know, this is also the case of Lean BTW: even if Lean recently became popular among mathematicians following Tom Hales' endorsement and Kevin's tremendous efforts to advertise it, the Lean developers initially wanted Lean to be a better proof assistant for verification, and I don't see why they would have forgotten about this objective.
Pierre-Marie Pédrot (Jun 22 2020 at 08:31):This schism between CS and math proofs seems utterly artificial to me
Théo Zimmermann (Jun 22 2020 at 08:32):It is something that comes regularly in discussions but only from the side of CS people. I believe this is due to the way the CS world is already fragmented in so many specialized ecosystems.
Pierre-Marie Pédrot (Jun 22 2020 at 08:33):if anything, I would have suspicions around mathematicians instead (preaching for my choir...)
Théo Zimmermann (Jun 22 2020 at 08:33):So it seems that more specialized tools are always needed and that this will result in a schism, but IMHO, specialized tools will continue to appear regularly, while mathematicians will use something that has already a large enough community...
Pierre-Marie Pédrot (Jun 22 2020 at 08:33):I have several mathematician friends who publicly expose a despise for anything computer related
Théo Zimmermann (Jun 22 2020 at 08:34):@Pierre-Marie Pédrot Well, that's precisely what Kevin is saying and why he's targeting so much of his efforts towards newborn mathematicians.
Pierre-Marie Pédrot (Jun 22 2020 at 08:35):right, but then I don't see the point on insisting that this is not CS, for god sake, this is math
Pierre-Marie Pédrot (Jun 22 2020 at 08:35):"your purity is safe"
Pierre-Marie Pédrot (Jun 22 2020 at 08:35):a proof is a proof
Pierre-Marie Pédrot (Jun 22 2020 at 08:36):don't mention CS and that's it
Alexander Gryzlov (Jun 22 2020 at 17:52):Kevin Buzzard said:
Alexander Gryzlov If you're right, where will Coq go? It has made some spectacular contributions in both areas. My feeling is that there are still some very basic questions which we don't understand though, when it comes to formalising undergraduate level mathematics. I've not seen a practical working definition of manifold robust enough to be usable to do undergraduate level example sheet questions yet -- in any theorem prover. If nobody can do undergraduate example sheets, no way will the maths researchers take any of these systems seriously.
IMO, Coq won't pick a side, as stated later in this thread. However we'll probably see some specialized tools making concrete decisions about their treatment of higher equalities. This can manifest simply as different modes within a single assistant of course.
Karl Palmskog (Jun 23 2020 at 11:31):in contrast to in math, I think it's very rare that "proofs win prizes" in CS (maybe in computational complexity?). For example, it would be absurd to say Milner got the Turing award for the SML type safety proof. Definitions are much more the "currency" in CS, and many/most proofs are long and boring.
Karl Palmskog (Jun 23 2020 at 11:38):in fancy HoTT jargon, propositional truncation in CS doesn't typically lose you all that much of interest - an opaque existential usually suffices
Paolo Giarrusso (Jun 23 2020 at 12:33):Typical syntactic programming language proofs are as boring as you describe, tho I expect most are not as boring as SML, but isn't that specific to PL/logic/"theory B"?
Alexander Gryzlov (Jun 23 2020 at 13:57):Paolo G. Giarrusso said:
Typical syntactic programming language proofs are as boring as you describe, tho I expect most are not as boring as SML, but isn't that specific to PL/logic/"theory B"?
What is "theory A"? :)
Karl Palmskog (Jun 23 2020 at 13:59):roughly corresponds to ICALP's tracks: https://easychair.org/cfp/ICALP-2020 (although I would call security etc. "Theory C")
Karl Palmskog (Jun 23 2020 at 14:02):I think "semantic" proofs can also be boring, let's say you're proving bisimulation with some super-fancy up-to relation without reference to a PL, can still have thousands of annoying uninsightful cases
Christian Doczkal (Jun 23 2020 at 15:27):@Alexander Gryzlov , If I'm not mistaken, the distinction dates back to the Handbook of Theoretical Computer Science which ships in two volumes:
The Handbook of Theoretical Computer Science provides professionals and students with a comprehensive overview of the main results and developments in this rapidly evolving field. Volume A covers models of computation, complexity theory, data structures, and efficient computation in many recognized subdisciplines of theoretical computer science. Volume B takes up the theory of automata and rewriting systems, the foundations of modern programming languages, and logics for program specification and verification, and presents several studies on the theoretic modeling of advanced information processing.
If someone has an older reference to this distinction (this is from 1994), I'd be happy to know.
Karl Palmskog (Jun 23 2020 at 15:40):one distinction in practice seems to be that theory A researchers call what they do "Theoretical Computer Science", but they are not keen to extend this label to theory B (whose researchers in my experience don't insist on or mention much the TCS label). Hence, I recall seeing TCS Stack Exchange moderation removing uses of "interactive proof" for proof assistant topics, since that term is reserved (so the user claimed) for Arthur-Merlin games and the like
Alexander Gryzlov (Jun 23 2020 at 15:40):Interesting, though I'd have probably placed automata in the complexity camp too
Karl Palmskog (Jun 23 2020 at 16:15):this is a funny perspective on Theory B from a Theory A researcher, very apt title: https://blog.computationalcomplexity.org/2009/03/lets-congradulate-gerard-huet-who.html --- comments are also quite fun I think
Alexander Gryzlov (Jun 23 2020 at 16:32):This also reminds me of the "Three tribes of programming" article (https://josephg.com/blog/3-tribes/).
Pierre-Marie Pédrot (Jun 23 2020 at 16:40):I did my PhD in the middle of the creation of the IRIF laboratory, which was the merge of a theory A lab (LIAFA) and a theory B lab (PPS)
Pierre-Marie Pédrot (Jun 23 2020 at 16:40):there was a clear border materialized by a stair, LIAFA being on the 4th floor and PPS on the 3rd
Pierre-Marie Pédrot (Jun 23 2020 at 16:41):you could feel the physical border when walking up the stairs :nuclear:
Paolo Giarrusso (Jun 23 2020 at 16:46):@Karl Palmskog maybe I misspoke, but with “semantics” I wasn’t thinking of bisimulation (or much about operational semantics), but rather denotational semantics or typical logical relations (even ones built on operational semantics), including realizability/saturated sets/parametricity/
Théo Zimmermann (Jun 23 2020 at 17:15):@Pierre-Marie Pédrot It feels much more integrated nowadays. Even if the PPS spirit remains there.
Last updated: Oct 03 2023 at 02:34 UTC