Proving for Fun

Stream: general

[maximilian p.l. haslbeck]

Dear Lean enthusiasts,

I'd like to advertise to you "Proving for Fun" -- an online platform where you can tackle proving challenges in your favorite proof assistant -- and ask for your help adding Lean as a supported language.

https://competition.isabelle.systems/competitions/contest/11/

This month's contest features freshly implemented support for Coq. This means you can now submit your solutions in both Isabelle and Coq. We want to support more ITPs and ACL2 is about to join. The contest is open until 9 August 2019.

Thanks to @Johannes Hölzl and @Kevin Kappelmann, we now also have a judging backend for Lean. We have translations for three of the tasks of this month's contest and they are up for your solutions. Please feel free to give feedback on the system and help translating the rest of the tasks; in the latter case please contact me here at zulip or via email (haslbema@in.tum.de).

This month's contest also serves as a warmup for the "Proof Ground" workshop, which
will take place in September alongside the ITP conference in Portland. The goal of the workshop is to bring together researchers from the ITP
community, to discuss and compete in a "proving contest", and it will use the Proving for Fun platform. If you happen to have ideas for
interesting tasks, please consider submitting them following our "Call for Problems".

We believe our problems should be a stimulating fun summer activity! We encourage you to participate and give us feedback on the prototype system.

Happy proving!

[Kevin Kappelmann]

Caveat: There is no support for mathlib (yet). Feel free to contribute here if you think that Lean without mathlib is the same as prohibiting the boxer the use of his fists.

[Alex J. Best]

Very cool, this is such a great idea! I think the lean system needs some extra checks adding though :rolling_on_the_floor_laughing: Screen-Shot-2019-07-30-at-15.31.26.png

[Kevin Kappelmann]

Oh oh, I assume that's a bug in my code and you did not actually break Lean :laughing: can you send me the code that made it pass so I can check what's wrong?

[Alex J. Best]

You are right I didn't break lean fortunately, its a bit cheeky:

notation `false` := true

theorem soundness_bug : false := trivial

[Kevin Kappelmann]

hahaha, damn! that's indeed very cheeky :big_smile:

[maximilian p.l. haslbeck]

hehe, yeah the task is called "Break the System" :), first time we confronted our colleagues with the Isabelle version of that task they came up with lots of ways to trick the system. I already expected that to happen for the first version of the lean judge. For Isabelle we have a blacklist of keywords that may not occur in the submission theory.

[maximilian p.l. haslbeck]

what keywords other than "notation" should be blacklisted for lean?

[Johan Commelin]

I paraphrase: "Lean without notation is the same as prohibiting the boxer the use of his fists."

[Chris Hughes]

I'm guessing the intended solution to the first problem wasn't 0, 500, 500

[maximilian p.l. haslbeck]

I'm guessing the intended solution to the first problem wasn't 0, 500, 500

ah, right, I just updated the Definition of pythagorean_triple, thanks

[Chris Hughes]

Now I have to prove 375^2 + 200^2 = 425^2 without mathlib. Looks like @Alex J. Best used the same trick as me, we both just moved down the leaderboard.

[Johan Commelin]

This is called "Proving for Fun" :interrobang:

[Johan Commelin]

¬mathlib → ¬calculator

[maximilian p.l. haslbeck]

so, we should add mathlib I guess? which version of it? is there an obvious choice?

[Alex J. Best]

Looks like Alex J. Best used the same trick as me, we both just moved down the leaderboard.

Unfortunately I wasn't that sneaky, but my proof was dependent on the original definition so it still broke :persevere:

[Johan Commelin]

Can't you use CI to always give users the latest and greatest?

[Johan Commelin]

Otherwise I would pick whatever the lean-3.4.2 branch points at right now.

[Johan Commelin]

I guess for most of these problems the basics of mathlib will suffice.

[Rob Lewis]

I think it would be very confusing for users if the mathlib version kept changing. Probably better to pick one and stick with it (for a while at least).

[Johan Commelin]

The next version of mathlib will ship a fun tactic that solves these exercises for you (-;

[maximilian p.l. haslbeck]

¬mathlib → ¬calculator

thanks to @Kevin Kappelmann mathlib (version 2019-07-31) is now available for the system, Lean version is: 3.4.2

[maximilian p.l. haslbeck]

if anybody is interested in translating the tasks "XOR" and "A funky grammar", please contact me! :) we can provide sample solutions in Isabelle and Coq!

[Kevin Kappelmann]

XOR and funky grammar.

[Kevin Buzzard]

They are surprisingly similar ;-)

[Kevin Buzzard]

Why can't we just do some collaborative effort here?

[Kevin Kappelmann]

They are surprisingly similar ;-)

Fixed :')

[maximilian p.l. haslbeck]

Why can't we just do some collaborative effort here?

I like the idea, but I can not see how to manage this. I'm reluctant to publish solutions before the contest ends. so I'd only like to disclose the solutions to someone who wants to do the translation.

[Kevin Buzzard]

Oh gosh I'm sorry, I hadn't internalised that this was still an open competition!

[maximilian p.l. haslbeck]

The "July 2019" contest at Proving for Fun is over now.
Congratulations to the winners and thanks to all the participants.
We hope you had some fun solving this month's problems and proving them formally.

We have set up a github repository with a summary of the contest, sample solutions and discussions about the problems. Feel free to participate in commenting any task in its issue and publishing your solution with a pull-request.

We specially want to thank the people who helped making the contest possible by creating the tasks and translating them to their proof assistant: Armaël Guéneau, Sebastiaan Joosten, Kevin Kappelmann, Simon Wimmer.

You still can submit your solutions for the tasks of the "July 2019" contest, they are now integrated into the "All Time" contest.

Tomorrow, Aug 13 at noon (MESZ) we start the "August 2019" contest which will be open until Sep 12 midnight. It also serves as a preparation for the contest happening at the Proof Ground workshop Sep 13 alongside the ITP conference in Portland.

[Kevin Buzzard]

The best Lean user were alexejbest shortly followed by chrishughes24 with 3 solved tasks: both solving two tasks with Lean and tricking our system.

Ha! Never trust a Lean user ;-)

[Kevin Buzzard]

(pointing out typo which is now fixed)

[maximilian p.l. haslbeck]

yeah, Aug 13 is correct ^^. thanks for pointing that out.

[Simon Hudon]

Is it still possible to use Lean to solve the problems?

[Kevin Kappelmann]

Yep, all problems will also be available in Lean :)

[Kevin Buzzard]

Many thanks Kevin! I see you were also involved with translating the previous problems into Lean

[maximilian p.l. haslbeck]

August 2019 Contest is open for submissions now. Have fun :) !

[Kevin Kappelmann]

...small Lean hiccup at the necklace problem. the check file needs to be corrected (submissions will automatically be re-graded for you) - sorry!

[Kevin Kappelmann]

...small Lean hiccup at the necklace problem. the check file needs to be corrected (submissions will automatically be re-graded for you) - sorry!

Now fixed - congrats @Chris Hughes for solving the first problem :)

[Chris Hughes]

Both statements for the second problem in Lean are false.

[Kevin Buzzard]

Maybe August's contest is supposed to be more challenging.

[Kevin Kappelmann]

Both statements for the second problem in Lean are false.

That's not great... :sweat_smile: did you make use of an uninhabited type by chance?

[Chris Hughes]

Yes

[Kevin Kappelmann]

Argh, types in Isabelle are always inhabited, which is why it makes more sense there.

[Kevin Buzzard]

rofl

[Kevin Buzzard]

I remember having this conversation with Manuel Eberl in Big Proof 2. I told him "We defined perfectoid spaces in Lean!" and he said "that sounds pretty simple, all you do is make a structure and prove that it's inhabited" and I said "oh gosh we're nowhere near proving that it's inhabited"

[Kevin Buzzard]

[since then we have proved that the empty space is perfectoid]

[Kevin Kappelmann]

I'll talk with @maximilian p.l. haslbeck and let you know if we change it to inhabited types only or change the task to disprove both. Nice work Chris :')

[Chris Hughes]

You don't actually even need to use uninhabited types to disprove both. prove is false with α = β = γ = bool and disprove is false with α = β = γ = unit

[Kevin Kappelmann]

I see, the Isabelle and Coq versions just do α = string, β = nat, γ = Prop, which isn't quite clear from the text. I guess we change it to that in Lean then as well.

[Kevin Kappelmann]

I hope this: lean_variables.zip should make sense now @Chris Hughes (I need to wait for Max to change it online).

[Chris Hughes]

Managed that one:+1:

[Kevin Kappelmann]

Legend! Sorry for the inconvenience - you are really really helpful! :) Again, your submission will re-run when the definition is fixed online.

[maximilian p.l. haslbeck]

Legend! Sorry for the inconvenience - you are really really helpful! :) Again, your submission will re-run when the definition is fixed online.

done that

[Simon Hudon]

I just submitted a solution which failed because "Illegal keyword "notation"". Are we allowed local notation?

[Alex J. Best]

Yes local should work I think

[Simon Hudon]

That's weird. It's still rejecting it.

[Simon Hudon]

... and I just noticed local notation `|` t `|` := fintype.card t at the beginning of the template file. Doubly weird

[Alex J. Best]

https://github.com/maxhaslbeck/proving-contest-backends/commit/915ab5e7cd1c6a3fd67b4ebc634ad5361b935d5b is where the code was added. Do you see anything in the regex there that explains it?

[Simon Hudon]

It looks like the comment mentioning notation is what is tripping it up. I just deleted that comment to check

[Simon Hudon]

Yuuup

[Simon Hudon]

The easiest fix would be to delete that comment from the template

[Kevin Kappelmann]

The easiest fix would be to delete that comment from the template

Thanks, we will remove it! Sorry for the trouble and congrats for being first to solve the problem! :)

[Kevin Kappelmann]

also congrats to @Alex J. Best for breaking the system (again!) :fireworks:

[Abhimanyu Pallavi Sudhir]

set_option pp.notation should be allowed, right?

[Chris Hughes]

You can always delete that before submission without breaking proofs.

[Kevin Kappelmann]

set_option pp.notation should be allowed, right?

It would be rejected at the moment. You can find the regex we use here. If someone has suggestions to improve this check (or anything else), let me know :)

[Andrew Ashworth]

I don't quite understand why checking is done via regex? You could call lean itself at trust level zero to check any proofs. How are things implemented on the back end?

[Abhimanyu Pallavi Sudhir]

set_option pp.notation should be allowed, right?

It would be rejected at the moment. You can find the regex we use here. If someone has suggestions to improve this check (or anything else), let me know :)

Just change the RegEx to ^notation?

[Kevin Kappelmann]

I don't quite understand why checking is done via regex? You could call lean itself at trust level zero to check any proofs. How are things implemented on the back end?

The compile/check commands are here. Setting the trust level to 0 is described as do not trust any macro and type check all imported modules. I do not know what is meant by "macro" in that setting. Also, would that mean that all imported mathlib files are type-checked again?

[Kevin Kappelmann]

set_option pp.notation should be allowed, right?

It would be rejected at the moment. You can find the regex we use here. If someone has suggestions to improve this check (or anything else), let me know :)

Just change the RegEx to ^notation?

you could then just add, for example, a whitespace, i.e. notation ... := ..., and it would succeed.

[Abhimanyu Pallavi Sudhir]

^\s*notation?

[Chris Hughes]

I don't quite understand why checking is done via regex? You could call lean itself at trust level zero to check any proofs. How are things implemented on the back end?

The compile/check commands are here. Setting the trust level to 0 is described as do not trust any macro and type check all imported modules. I do not know what is meant by "macro" in that setting. Also, would that mean that all imported mathlib files are type-checked again?

I think yes. The default trust setting is max. This could be changed on the mathlib binaries.

[Kevin Kappelmann]

^\s*notation?

That just solves the whitespace case. You can also have things like #print "Let's cheat" notation 'false' := true

[Kevin Kappelmann]

I think yes. The default trust setting is max. This could be changed on the mathlib binaries.

Hmm, I do not know how to tweak the compile process such that mathlib is trusted and the submission file is not. Are there any references where I can learn how to do that?

[Sebastian Ullrich]

I don't think trust 0 gets you anything if you compile the submission yourself anyway. On the other hand, to be completely safe you should probably put the theorem statement in a separate file that doesn't import the submission. Then you can do something like

import .statement
import .submission

theorem yesitstrue : _root_.thestatement := theproof

[Kevin Kappelmann]

I don't think trust 0 gets you anything if you compile the submission yourself anyway. On the other hand, to be completely safe you should probably put the theorem statement in a separate file that doesn't import the submission. Then you can do something like

import .statement
import .submission

theorem yesitstrue : _root_.thestatement := theproof

Ah, that's a good idea to solve the notation issue - thanks! :)

[Sebastian Ullrich]

Though I guess someone could still add a notation for _root_.thestatement, haha. So you should beat them to it and define your own notation:
statement.lean

def statement := ...
notation `statement` := statement

check.lean

import .statement
import .submission

theorem yesitstrue : statement := theproof

Now a malicious actor can at most overload statement, which will fail elaboration. At least that's the last trick I can think of.

[Rob Lewis]

Or you could do the test with a metaprogram. Write a tactic that retrieves the declaration named thestatement and check that the type of theproof unifies with the body of that declaration.

[Sebastian Ullrich]

You still have to call the tactic somewhere. There will be at least one identifier exposed to the attacker, so wrapping it in a notation is the best I can come up with

[Rob Lewis]

You can inline the tactic in a run_cmd, no?

[Rob Lewis]

Or even define the tactic in statement.lean and just call it with a run_cmd in check.lean.

[Sebastian Ullrich]

Yes, and then I'll shadow your tactic call in check.lean with a notation for tactic.skip in my submission :)

[Rob Lewis]

Ah, yeah, of course.

[Rob Lewis]

I did a low tech version of this for checking homework assignments in my course this spring. It definitely wasn't secure, but I figured if any students learned enough about Lean to trick it, they deserved the points anyway.

[Kevin Buzzard]

Do you do anything about the trick Gabriel Ebner raised whereby a malicious piece of Lean code can delete all the files on your computer?

[Kevin Buzzard]

I think it was once a Lean issue?

[Rob Lewis]

I remember having that discussion at Big Proof 1. Any programming language can do this, but Lean is kind of special in that code gets executed as soon as you open it in the editor.

[Rob Lewis]

https://github.com/leanprover/lean/issues/1781

[Mario Carneiro]

The regex looks very fragile to me. I think this is still possible:

namespace tactic.interactive
open lean.parser
@[user_command] meta def evil_cmd (_ : interactive.parse $ tk "evil") : lean.parser unit :=
with_input command_like ("nota" ++ "tion `false` := 0 = 0") >> return ()
end tactic.interactive
evil

theorem contradiction : false := rfl

[Kevin Kappelmann]

I'd say, just try it out! and if it works, please hide the solution :')

[Sebastian Ullrich]

I had forgotten that we allow whitespace inside tokens... to be honest, there probably is no simpler bullet-proof solution than parsing the export format. If you put the theorem statement in a separate import, you "just" have to check that the type of the exported definition is a constant expression of the statement type's name.

[Alex J. Best]

Yeah maybe that is easier, from my experiments yesterday breaking it (sorry @Kevin Kappelmann ), regex is hard to get perfect and esp. with lean's syntactic complexity ruling out all the edge cases sounds like it might take a little while, maybe the internal format is the way to go.

[Floris van Doorn]

I've been also thinking how to make this robust. Maybe this works:
As @Sebastian Ullrich suggested have a separate file statement.lean, which contains the statement, but does not import submission.lean. To make it robust, how about we generate a random name with 16 random letters (different for every time someone submits), and then:

statement.lean

def <random_name> := false

check.lean

import .statement .submission

theorem yesitstrue : <random_name> := soundness_bug

Does anyone know an attack against that?

[Rob Lewis]

.submission could have a metaprogram that reads the file statement.lean and tries to parse the name.

[Kevin Kappelmann]

If I understand correctly, in Isabelle, they save the statement context in a local file and then load that file in .submission - see here page 4

[Kevin Buzzard]

This thread should be renamed "cheating for fun"

[Kevin Kappelmann]

Sebastian's proposal seems to be the easiest, most reliant option so far to me.

[Kevin Kappelmann]

btw, we got a Lean winner! :muscle: congrats @Simon Hudon

[Simon Hudon]

Thanks :)

[Floris van Doorn]

I want to PR the lemmas I used in these exercises to mathlib, but I also don't want to give hints to other provers... I guess I'll wait till mid-September.

[Simon Hudon]

You can try giving the proof by trust_me

[Floris van Doorn]

(deleted - that moment when "Reply" doesn't reply to the bottom message in your stream :P)

[David Michael Roberts]

[since then we have proved that the empty space is perfectoid]

What's the terminal perfectoid space, if there is one? Some analogue of Spec(Z)?

[Kevin Buzzard]

There won't be one. There are perfectoid fields of char 0 and perfectoid fields of char p, maybe there is some weird pathological object. But it's not the right question. People work with perfectoid spaces over a fixed perfectoid field and over that field you just look at the affinoid space attached to that field. The problem is that we have no examples of perfectoid fields yet even though they're do-able -- we just need more algebra and field theory in Lean and more people

[Johan Commelin]

@David Michael Roberts I think that nowadays the answer is: perfectoid spaces embed into the category of diamonds. And there is no terminal diamond, which is a feature. Because now you can look at Spa Q_p × Spa Q_p and it will not be Spa Q_p. (Philosophically, this means that we now think that we know how to take p-adic fibre products over $\mathbb{F}_1$.)

[Kevin Kappelmann]

Given the following file test.lean

axiom «quot.sound : a» : false
theorem broken : false := «quot.sound : a»

When I run

lean test.lean -E check.out --json --only-export=broken
leanchecker check.out broken

the output of leanchecker is

axiom quot.sound : false
theorem broken : false
checked 12 declarations

I would have expected to have the first line say something like axiom «quot.sound : a» : false. Is this a bug or working as expected? @Alex J. Best came across this while checking the fix I committed for the proving for fun competition. We are detecting non-built-in axioms, e.g. everything besides propext, classical.choice, quot.sound, by parsing the output of leanchecker. In this case, we would not be able to detect any cheat.

[Sebastian Ullrich]

Now I'm even more convinced that you should parse the export file yourself :)

[Alex J. Best]

Maybe one alternative is to use https://github.com/gebner/trepplein I just tried it and with --print-all-decls I see axiom quot.sound : a : false for the above example.

[Alex J. Best]

Or better yet, run both!

[Keeley Hoek]

right, and then you could just prohibit the declaration of any extra axioms?

[Alex J. Best]

Yes, trepplein helpfully prints /- builtin -/ before any builtin axioms so that seems easier in this case.

[Kevin Kappelmann]

I had a brief look at trepplein, but I do not want to install scalar, sbt, etc. as well when setting up the backend (installing trepplein actually failed for me at first because there is a bug with JDK10 and optimisations). I just included the type of the axiom in the check for now

[Kevin Kappelmann]

Thanks for all the help, that is breaking my code multiple times @Alex J. Best

[Alex J. Best]

Thanks for putting up with me! It looks pretty robust now.

[Kevin Buzzard]

Hey what is happening with Proving for Fun this month? The current competition is about to end. Will the new one support Lean? @Kevin Kappelmann do you know about this stuff?

[Kevin Buzzard]

I've been trying the August 2019 problems and some are infuriating.

[Kevin Buzzard]

Am I allowed to import stuff which isn't imported yet? I don't have use in the PCP problem.

[Alex J. Best]

Yes you should be able to import anything from mathlib

[Andrew Ashworth]

do solutions for these problem get released at the end of the month? I'm interested in comparing across provers

[Alex J. Best]

Yes: see https://github.com/maxhaslbeck/ProvingForFun-July2019 for July's. Also there is another solution in the "issues" tab there that is not saved as a file.

[Alex J. Best]

There are no lean ones on there yet though, just one of @Chris Hughes on the issues page

[Kevin Buzzard]

Maybe this will change on Saturday :-)

[Kevin Kappelmann]

Hey what is happening with Proving for Fun this month? The current competition is about to end. Will the new one support Lean? Kevin Kappelmann do you know about this stuff?

@Kevin Buzzard There is in fact a whole workshop including a new competition tomorrow at ITP. You can again solve all problems in Lean, Isabelle, or Coq. Moreover, you can discuss, for example, how to organise, improve, and make use of proving contests to help spark interest for the ITP community at the workshop :) (I'm sadly not at ITP, but @maximilian p.l. haslbeck will be)

[Kevin Kappelmann]

do solutions for these problem get released at the end of the month? I'm interested in comparing across provers

Yes, solutions will be released at the end of the month. If @Chris Hughes does not mind, I can provide his Lean solutions in the July repository. At the end of the August competition, I suppose that Max will create a similar repository including sample solutions.

[Chris Hughes]

I don't mind. They're not necessarily particularly elegant solutions.

[Kevin Kappelmann]

Yes: see https://github.com/maxhaslbeck/ProvingForFun-July2019 for July's. Also there is another solution in the "issues" tab there that is not saved as a file.

I uploaded the solutions for the two problems that were formalised in Lean now; they are quite simple though. The ones for August gonna be more interesting.

[Kevin Buzzard]

I just finished PCP but looks like I missed the deadline :D I got caught out by the fact that I'm not in the right time zone ;-)

[Andrew Ashworth]

Thank you for uploading the solutions. I feel like having a collection of worked examples in multiple languages is very educational. Maybe we need a Rosetta Code for theorem proving... http://rosettacode.org

[Andrew Ashworth]

Sort of like Freek's 100 problems list but more general

[Kevin Buzzard]

Thanks for adding the Lean formalisations of the July questions! Can I somehow upload my solution to PCP (August) even though the deadline is passed? Or have I missed my chance?

[Kevin Buzzard]

By the way, when I download the zip files, I always have to rename the names of the Lean files, e.g. from Defs.lean to defs.lean (or else the import fails). I'm on Ubuntu.

[maximilian p.l. haslbeck]

I just finished PCP but looks like I missed the deadline :D I got caught out by the fact that I'm not in the right time zone ;-)

The PCP task is now in the "Alltime Contest", fell free to submit your solution there.

[Kevin Kappelmann]

By the way, when I download the zip files, I always have to rename the names of the Lean files, e.g. from Defs.lean to defs.lean (or else the import fails). I'm on Ubuntu.

That's very true and inconvenient - I created an issue on GitHub

[maximilian p.l. haslbeck]

Today we will have the Proof Ground workshop here in Portland. We will have two contests, one before lunch (10:30 - 12:30 (PDT)) and one after lunch (14:00 - 15:30 (PDT)). Feel free to participate from anywhere on earth and have fun by solving and mechanizing the tasks :).

[maximilian p.l. haslbeck]

The morning session is starting now. You can see the problems here and submit solutions: https://competition.isabelle.systems/competitions/contest/13/

[maximilian p.l. haslbeck]

The afternoon session has started. https://competition.isabelle.systems/competitions/contest/14/

[Andrew Ashworth]

Looks like sledgehammer_squad completed every problem! How much of their proofs was via sledgehammer as opposed to human reasoning?

[Simon Hudon]

They were clever in how they broke down the problem between the two of them and sledgehammer allowed them to skirt detailed proofs

[Andrew Ashworth]

Do you know which part of sledgehammer was the most effective?

[Andrew Ashworth]

as in was their a particular solver it called out to that solved most of their intermediate lemmas

[Scott Morrison]

What the business with

-- the goal used in submission
notation `GOAL` :=

in the Lean template. Am I meant to be confused by this?

[Manuel Eberl]

I can tell you that I at least didn't use sledgehammer very much. Occasionally when I was too lazy to figure out what lemmas I need for some obvious fact. But I don't use it that much because it breaks my flow if I have to wait for it to finish.

[Manuel Eberl]

We only worked on one problem in parallel, and there sledgehammer did probably save us a few minutes because it made the "integration" of my lemmas and Peter's proof that wanted to use them easier.

[Manuel Eberl]

In any case, the difficult part is figuring out what auxiliary lemmas you need, what kind of induction pattern to use, and then you sometimes have to do ugly case distinctions. Sledgehammer doesn't help with any of that. So the role of sledgehammer in our work today really shouldn't be overestimated.

[Simon Hudon]

Thanks for chiming in @Manuel Eberl. It is quite impressive what a head start you two had. Any idea what was most determinant in your performance?

[Andrew Ashworth]

oh - is it weird that I'm actually a little disappointed? I was hoping there was going to be "that one secret tactic that computer scientists don't want you to know about" that would solve my proofs. But, like always, the solution is: think really hard and be a smarter human, which is difficult work as you know, haha

[Manuel Eberl]

Thanks for chiming in Manuel Eberl. It is quite impressive what a head start you two had. Any idea what was most determinant in your performance?

Hard to say. The automation probably helped a lot. Also I have 8 years of experience with the system, and Peter even more.

[Manuel Eberl]

I think the real question is: What obstacles did the other teams encounter?

[Manuel Eberl]

The grammar problem and the "fold" one were a bit tricky, but the others were fairly straightforward. So I think the best strategy is to figure out where the other teams go stuck with those simple problems and why.

[Manuel Eberl]

Floris's team was only a few minutes behind us in the first session. I'll ask him what the problem was in the second session. I'm curious myself.

[Simon Hudon]

Speaking for Floris' team, in the second round, we didn't split the workload smartly and when we got stuck we didn't switch problems. Some simple ideas also escaped us.

[Mario Carneiro]

@Floris van Doorn Here's the "slick" proof I was thinking of for the balanced words challenge:

import data.list.basic data.nat.basic

inductive balanced : list bool → Prop
| empty : balanced []
| app {x y} : balanced x → balanced y → balanced (x ++ y)
| tf {l} : balanced l → balanced (tt :: l ++ [ff])
| ft {l} : balanced l → balanced (ff :: l ++ [tt])

theorem balanced.mk' : ∀ b {l}, balanced l → balanced (bnot b :: l ++ [b])
| tt _ := balanced.ft
| ff _ := balanced.tf

inductive unbalanced (b : bool) : list bool → ℕ → Prop
| bal {} {l₁ l₂} : balanced l₁ → balanced l₂ → unbalanced (l₁ ++ b :: l₂) 0
| up {} {l₁ l₂ n} : balanced l₁ → unbalanced l₂ n → unbalanced (l₁ ++ b :: l₂) (n.succ)

theorem unbalanced.app {b l₁ l₂ n} (h₁ : balanced l₁) (h₂ : unbalanced b l₂ n) :
  unbalanced b (l₁ ++ l₂) n :=
begin
  induction h₂ with l₂ l₃ h₂ h₃ l₂ l₃ n h₂ h₃ IH; rw ← list.append_assoc,
  { exact unbalanced.bal (h₁.app h₂) h₃ },
  { exact unbalanced.up (h₁.app h₂) h₃ }
end

inductive tipsy (l : list bool) : ℕ → ℕ → Prop
| left (m k) : unbalanced tt l k → tipsy (m + k).succ m
| right (m k) : unbalanced ff l k → tipsy m (m + k).succ
| bal {m} : balanced l → tipsy m m

theorem lem1 : ∀ {l m n}, m = n → tipsy l m n → balanced l
| l _ _ _ (tipsy.bal h) := h
| l _ _ e (tipsy.left m k _) := (ne_of_gt (nat.lt_succ_of_le (nat.le_add_right _ _)) e).elim
| l _ _ e (tipsy.right m k _) := (ne_of_lt (nat.lt_succ_of_le (nat.le_add_right _ _)) e).elim

theorem lem2a {b l n} (h : unbalanced b l n) :
  (nat.cases_on n (balanced (bnot b :: l)) (unbalanced b (bnot b :: l)) : Prop) :=
begin
  cases h with l₁ l₂ h₁ h₂ l₁ l₂ n h₁ h₂,
  { simpa using (h₁.mk' b).app h₂ },
  { simpa using h₂.app (h₁.mk' b) },
end

theorem lem2b {b l} (h : balanced l) : unbalanced b (b :: l) 0 :=
unbalanced.bal balanced.empty h

theorem lem2c {b l n} (h : unbalanced b l n) : unbalanced b (b :: l) (n.succ) :=
unbalanced.up balanced.empty h

theorem lem2 {l} : tipsy l (l.count tt) (l.count ff) :=
begin
  induction l with b l IH, {constructor, constructor},
  cases b, all_goals {
    simp [-add_comm],
    generalize_hyp : l.count tt = m at IH ⊢,
    generalize_hyp : l.count ff = n at IH ⊢,
    cases IH },
  { cases IH_k,
    { constructor, exact lem2a IH_a },
    { rw [← nat.succ_add], constructor, exact lem2a IH_a } },
  { rw [← nat.add_succ], constructor, exact lem2c IH_a },
  { exact tipsy.right _ 0 (lem2b IH_a) },
  { rw [← nat.add_succ], constructor, exact lem2c IH_a },
  { cases IH_k,
    { constructor, exact lem2a IH_a },
    { rw [← nat.succ_add], constructor, exact lem2a IH_a } },
  { exact tipsy.left _ 0 (lem2b IH_a) }
end

theorem goal {l} : balanced l ↔ l.count tt = l.count ff :=
⟨λ h, by induction h; simp [*, -add_comm], λ h, lem1 h lem2⟩

[Kevin Kappelmann]

Hope you guys had fun and maybe discussed some ideas how to further extend and make use of the competitions system!

What the business with

-- the goal used in submission
notation `GOAL` :=

in the Lean template. Am I meant to be confused by this?

This was done to prevent the "notation cheat". See this post.

[Scott Morrison]

Could we maybe have a comment to the effect that it's irrelevant implementation garbage, that someone interested in doing the problem should ignore?

[Scott Morrison]

(deleted)

[Floris van Doorn]

@Mario Carneiro That's a slick proof indeed. Very nice!

[Kevin Buzzard]

@Manuel Eberl posted a link to his proofs for Proof Ground 2019 on Twitter. I'd like to have a discussion about some of those problems, and in particular why some of them might be harder in Lean than in Isabelle. But I keep not starting it because I've not finished all the questions yet :-)

[Mario Carneiro]

I haven't seen these proofs yet but I think you probably will get only a weak signal regarding overall ease of use of the library from a 3 hour competition. You are far more likely to see noise relating to how well the competitor knows the library and the right proof strategy for the competition problems

[Simon Hudon]

That's also my opinion

[Alexandre Rademaker]

In the experiments I am doing with large theories, I believe it would be nice to have something similar to Sledgehammer in Lean. The proof https://github.com/arademaker/sumo/blob/lists/bs.lean#L178-L210 is just a sequence of uses of the same 2-3 axioms to navigate in the SUMO hierarchy.

[Floris van Doorn]

The discussion about Codewars sparked me to try to break the system again. It is still possible: https://github.com/maxhaslbeck/proving-contest-backends/issues/27

[Kevin Kappelmann]

War. War never changes...

[Alexandre Rademaker]

Andrew Ashworth said:

Thank you for uploading the solutions. I feel like having a collection of worked examples in multiple languages is very educational. Maybe we need a Rosetta Code for theorem proving... http://rosettacode.org

My first contribution. I have also created a page for Lean. See

http://rosettacode.org/wiki/Fibonacci_sequence#Lean

[Alexandre Rademaker]

The competitors are taking their turn... https://rosettacode.org/wiki/Category:Isabelle. ;-)

[Kevin Buzzard]

I don't think of these other systems as competitors. I believe that early lean development was hugely inspired by Isabelle. I think the interesting question is what does and doesn't work in the systems (or more precisely how well various parts of methods work in the systems). Isabelle has demonstrated that complex analysis works great there. I am unclear about whether there is a serious Coq development but we have essentially nothing in Lean. Perhaps if the Isabelle people explain how to do it, we can learn!

[Alexandre Rademaker]

Hi @Kevin Buzzard surely. I was just making some fun. I completely agree that we can and must learn from each other. Regarding the rosettacode.org, I like the idea of the webiste. Having the same problem encoded in many different tools/language help us understand the differences. That is why I am motivating people to contribute with more Lean code. Next I would like to try the sort algorithms that already have Isabelle code there.