Proof Ground 2020

Stream: general

[maximilian p.l. haslbeck]

Dear Lean enthusiasts,

we are organizing another edition of the proving competition workshop "Proof Ground", which will take place virtually.
Please notice our Call for Problems, and spread the word!

---

Call for Problems

---

Proof Ground 2020
Interactive Proving Contest
June 29, 2020
https://www21.in.tum.de/~wimmers/proofground/

---

at IJCAR 2020
International Joint Conference on Automated Reasoning
June 29 - July 5, 2020, (originally in) Paris, France, now fully virtual
https://ijcar2020.org/

---

This workshop brings together researchers of the ITP community to compete in a "proving contest".

While programming contests (e.g. ACM ICPC, International Olympiad in Informatics) challenge large numbers of participants to solve algorithmic problems within a short time, we envision proving contests to entice proof engineers to formally prove small but interesting problems from mathematics or computer science.

A contest system is currently used for teaching and hosting proving contests in Coq, Isabelle, and Lean.

Proof Ground 2020 is part of the Paris Nord Summer of LoVe 2020, a joint event on LOgic and VErification at Université Paris 13, made of Petri Nets 2020, IJCAR 2020, FSCD 2020, and over 20 satellite events.

As the main conferences of Paris Nord Summer of LoVe will happen as virtual conferences due to the Covid-19 outbreak, Proof Ground will also take a purely virtual format.

The first edition of the workshop has been held at ITP 2019.

Important Dates

• Submission deadline: June 1, 2020

• Workshop and Competition: June 27, 2020

Call for Problems

In order to conduct a stimulating contest we solicit interesting tasks.

A contest typically lasts for two hours and consists of around five problems with varying difficulty.

A problem:

• should contain an informal statement of the problem together with a
  template for the formal proof;

• should come with a reference solution (in any ITP);

• should be solvable (including formal proof) within 30 minutes;

• should be easy to state in any proof assistant, without requiring
  too much background library;

• could be from any part of mathematics, software verification, or
  your daily work with ITPs, and could also be a logic puzzle/riddle;

• could contain several subproblems which lead to partial points.

Submissions from (potential) competition participants are allowed.

Examples can be found at the current "Proving for Fun" contest system, e.g. here.

Submissions can be made via email to wimmers [at] in [dot] tum [dot] de by the date indicated above.

Organizers

Maximilian P. L. Haslbeck
Tobias Nipkow
Simon Wimmer

[Andrew Ashworth]

Maybe this could be cross-posted to the #Codewars stream since it is related

[Andrew Ashworth]

Alternatively the proof grounds problems might be reasonable kata :upside_down:

[maximilian p.l. haslbeck]

Next Monday June 29th, we will have a proving contest during the Proof Ground 2020 workshop .
The workshop is affiliated with the International Joint Conference on Automated Reasoning (IJCAR) which was originally planned to take place in Paris but now happens fully virtually (in timezone GMT+2).
As such, participation in the conference as well as the workshop and competition is free and open to anyone.

[maximilian p.l. haslbeck]

We prepared some nice problems for you, provide task statements in Coq, Lean and Isabelle and hope you will have fun solving them. The competition on Monday is split into two sessions. To participate in the competition, you only need an account at the competition site. After the contest, the tasks will also appear in the "AllTime" contest, where you can already find many tasks to prepare for Monday :).

[maximilian p.l. haslbeck]

As the competition will happen online, it is hard to encourage team work. So we decided to require participation as individuals for this year's edition. Of course there is no way to check that, so we trust your fairness.

[maximilian p.l. haslbeck]

Before and after the contest we will have short meetings via Zoom to clarify questions and discuss results. Also we will host virtual "coffee breaks" where you can chat with other participants and discuss your approaches. We are curious to see how this will work out. Anyway, if you want to participate in the Zoom calls and coffee breaks, it's best to register for the workshop via IJCAR.

[maximilian p.l. haslbeck]

Albeit we are fixed to schedule the workshop in Central European Summer Time, we encourage people from all over the world to participate in the contest, or at least one of the sessions.

[Kevin Buzzard]

The "developing and submitting Solutions" section on the competition.isabelle.systems website just has instructions for how to submit in Isabelle. What version of Lean and Mathlib are going to be used tomorrow? Should I set up some bare repo and stub files in src called Defs.lean, Check.lean and Submission.lean?

Unrelated: I just registered for the workshop now. Will I get an email Zoom link at some point?

[Reid Barton]

I got an email with Zoom links about 2 hours ago, I can send it to you.

[Kevin Kappelmann]

Unless they upgraded the versions since I published an update, it will be mathlib version/rev eb5b7fb7f406385cd1f2efaa15d9c0923541b955 and lean 3.16.2

[Kenny Lau]

https://competition.isabelle.systems/competitions/contest/18/leaderboard/

[Kenny Lau]

lol I'm the only one who only completed Task 2

[Reid Barton]

that one was gross

[Reid Barton]

I abandoned 1 because the Lean formulation was buggy :frown:

[David Wärn]

The Lean formulation of 1 is true for trivial reasons...

[Reid Barton]

Yeah I submitted feedback and thought they might fix it but apparently not...

[Reid Barton]

Obviously the first part of 2 was intended to help somehow with the second part, but I didn't see how...?

[Sebastian Ullrich]

There's no way to see the leaderboard without registering...?

[David Wärn]

Reid Barton said:

Obviously the first part of 2 was intended to help somehow with the second part, but I didn't see how...?

I guess you write a nonempty list as [x .. x] ++ xs, where xs is empty or has a head different from x, and then use the first part on the reversal reverse xs ++ [x .. x]?

[Kevin Buzzard]

leaderboard.png

[Kevin Buzzard]

Q3 was a maths question, the other two were CS. But you can guess this by looking at which systems solved which problems

[Reid Barton]

For problem 2 I said to myself "I need listlib not mathlib"

[Reid Barton]

Also problem 2 isn't CS.

[Reid Barton]

Welp two more problems about lists

[Mario Carneiro]

This seems to be a recurring problem on Proof Ground - the problems aren't written/selected by lean users and so suffer both from lack of fit and also unnatural formalization. What's with all the CS slant?

[Mario Carneiro]

I also want to see the problems turned into an untimed code golf competition after the main competition (including fixing the theorem statements). It can also be something other than code golf, just show off your solution and collectively find the "right" / "elegant" way to do the problem. That would do well as decompression and it's also a good way to learn

[Reid Barton]

it would be nice as well if they would check the problem statements beforehand or at least notify contestants if they change the problem mid-contest

[Floris van Doorn]

Yes, they announced that on Discord 15 minutes ago... :/

[Floris van Doorn]

Also, in the first problem, judge1 contains xs ≠ ys ∧ xs.length = ys.length ∧ .... I believe that neither of the first two conjuncts should be there...

[Floris van Doorn]

just curious: what was wrong with theNodes formulation in Lean? The original problem and the fixed problem seem equivalent to me.

[Reid Barton]

One of the lemmas had an argument n which shadowed the global n making it false

[Reid Barton]

I don't know if there was any other reason for the change

[Alex J. Best]

David Wärn said:

The Lean formulation of 1 is true for trivial reasons...

And this, what was wrong there?

[Reid Barton]

Also, I'm not sure what the point of the last lemma was supposed to be, but it was false also and then deleted

[Reid Barton]

Alex J. Best said:

David Wärn said:

The Lean formulation of 1 is true for trivial reasons...

And this, what was wrong there?

There was nothing restricting the processes to the range [0, N). So the statement was trivial because there was no way for infinitely many processes to finish.

[Reid Barton]

It's clear there could not have been a Lean solution to either of these problems

[Floris van Doorn]

ah

[Alex J. Best]

Oh lol!

[Patrick Massot]

What kind of contest is this if nobody tries to do the problems before the contest?

[Kevin Buzzard]

It's a contest where they probably have very few people to test everything

[Simon Hudon]

I was behind a part of the Lean formulation. It could have used more of my attention and time

[Simon Hudon]

I hope it was still an interesting challenge

[Manuel Eberl]

Sheesh, that's quite a lot of negativity in here.

Mario Carneiro said:

This seems to be a recurring problem on Proof Ground - the problems aren't written/selected by lean users and so suffer both from lack of fit and also unnatural formalization. What's with all the CS slant?

Well, Lean users were and still are welcome to submit problems. And I would imagine there was only one ‘mathematical’ problem because nobody submitted ‘mathematical’ problems. I think it might also be more difficult to find ones that are suitable for the competition setting. There are a lot of constraints: They have to be doable with the standard library of all three systems, they shouldn't be too difficult, but it also shouldn't be something that's so standard that it's already in a library somewhere.

I also find it a bit strange that several people have said things like "Lean = mathematical system, Isabelle = CS" system. I don't see any indication for that. Isabelle has a huge amount of maths and quite a few people working on formalising maths in it. I was probably the only one of those active in the competition, but I think that's more an artefact of the competition (only a negligible fraction of the ITP community took part in it) and does not say anything about the systems themselves.

The problem with the Lean version of the problems (which I haven't really looked into so I cannot comment on it) was unfortunate, but at the end of the day, that is the sort of thing that can only be reliably checked by Lean experts. For instance, you cannot expect people who have zero connection to Lean to make a sample solution in Lean.

(By the way, the concurrency task also had some problems in Isabelle related to "undefined" processes being able to make steps, but it was still provable.)

Oh and by the way, no, I am not an organiser. They're just my friends and colleagues and I think this thread has been a bit unfair towards them. If the Lean community feels that PG has an ‘anti-Lean’ slant, I suggest more people from the Lean community contribute and problems and sort out technical issues next time to correct that.

[Manuel Eberl]

Oh and by the way, last year, I was asked on here whether sledgehammer was important for me during the competition. It wasn't last year, but this year, it absolutely was. Saved me quite a bit of time! I even solved subtask 5.2 (the first part of the good node characterisation) without even understanding what the statement said, it was just "induction, auto, sledgehammer" and it was done.

[Reid Barton]

Problem domains are a matter of taste. But making sure the problems are solvable is a basic part of running a contest. If the organizers don't want to write solutions for the Lean translations then they should not claim to support Lean.

[Reid Barton]

The communication with contestants also seemed poor from my perspective. I submitted a comment about the concurrency task being mistranslated into Lean and never heard anything, nor did the task statement change--I don't know if a human ever saw my message. On the other hand the nodes task changed silently (in a way guaranteed to break any solution badly) near the end of the contest. Apparently it was announced on some discord but I didn't know about it until after the contest.

[Reid Barton]

I was excited about this contest, enough to wake up at 4:30 AM local time. But it ended up being a waste of my time.

[Reid Barton]

I can't speak for others, but I hope you can understand why my experience with this particular event was quite negative.

[maximilian p.l. haslbeck]

I'd like to comment on that as an organizer. Regarding the untested Lean template, I guess that was mainly our fault in time management: the Problem Committee, which includes Lean users, had only 10 days to translate the tasks. As we had four problems already in Isabelle and two in Coq, the workload for Lean apparently was too much. For the next edition we definitely will reserve more time for the translations and we invite you to take part in it!

[maximilian p.l. haslbeck]

We invite you to follow the Call for Problems, which might result in more problems with mathematical flavour and more natural formalization in Lean. I think we will organize the next edition with ITP 2021 in Rome (?). We'd like to cooperate here to generate a fun and stimulating experience.

[maximilian p.l. haslbeck]

As for the poor communication: it's only the second time we organize this competition -- first time virtual. but you are right. I'm sorry for the last minute changes in the nodes task.

[maximilian p.l. haslbeck]

I hope next time we can host a contest where you are again excited enough to wake up at 4:30 AM :).

[maximilian p.l. haslbeck]

As a step forward, who of you could help out fixing the task statements of the competition for Lean; such that we can use them in the AllTime contest on Proving for Fun?

[Mario Carneiro]

I'm willing to volunteer to review the problem statements