Zulip Chat Archive

Stream: general

Topic: Proof Ground 2020


view this post on Zulip maximilian p.l. haslbeck (May 11 2020 at 16:58):

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

view this post on Zulip Andrew Ashworth (May 13 2020 at 03:36):

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

view this post on Zulip Andrew Ashworth (May 13 2020 at 03:37):

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

view this post on Zulip maximilian p.l. haslbeck (Jun 24 2020 at 15:31):

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.

view this post on Zulip maximilian p.l. haslbeck (Jun 24 2020 at 15:31):

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 :).

view this post on Zulip maximilian p.l. haslbeck (Jun 24 2020 at 15:31):

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.

view this post on Zulip maximilian p.l. haslbeck (Jun 24 2020 at 15:31):

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.

view this post on Zulip maximilian p.l. haslbeck (Jun 24 2020 at 15:31):

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.

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 19:06):

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?

view this post on Zulip Reid Barton (Jun 28 2020 at 19:07):

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

view this post on Zulip Kevin Kappelmann (Jun 28 2020 at 21:42):

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

view this post on Zulip Kenny Lau (Jun 29 2020 at 10:30):

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

view this post on Zulip Kenny Lau (Jun 29 2020 at 10:30):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 10:33):

that one was gross

view this post on Zulip Reid Barton (Jun 29 2020 at 10:33):

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

view this post on Zulip David Wärn (Jun 29 2020 at 10:40):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 10:41):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 11:09):

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

view this post on Zulip Sebastian Ullrich (Jun 29 2020 at 11:11):

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

view this post on Zulip David Wärn (Jun 29 2020 at 11:18):

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]?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:23):

leaderboard.png

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:24):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 11:25):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 11:33):

Also problem 2 isn't CS.

view this post on Zulip Reid Barton (Jun 29 2020 at 12:02):

Welp two more problems about lists

view this post on Zulip Mario Carneiro (Jun 29 2020 at 12:13):

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?

view this post on Zulip Mario Carneiro (Jun 29 2020 at 12:19):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 13:29):

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

view this post on Zulip Floris van Doorn (Jun 29 2020 at 13:31):

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

view this post on Zulip Floris van Doorn (Jun 29 2020 at 13:33):

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...

view this post on Zulip Floris van Doorn (Jun 29 2020 at 14:12):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 14:12):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 14:12):

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

view this post on Zulip Alex J. Best (Jun 29 2020 at 14:13):

David Wärn said:

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

And this, what was wrong there?

view this post on Zulip Reid Barton (Jun 29 2020 at 14:13):

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

view this post on Zulip Reid Barton (Jun 29 2020 at 14:14):

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.

view this post on Zulip Reid Barton (Jun 29 2020 at 14:14):

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

view this post on Zulip Floris van Doorn (Jun 29 2020 at 14:14):

ah

view this post on Zulip Alex J. Best (Jun 29 2020 at 14:17):

Oh lol!

view this post on Zulip Patrick Massot (Jun 29 2020 at 14:24):

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

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 14:37):

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

view this post on Zulip Simon Hudon (Jun 29 2020 at 14:41):

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

view this post on Zulip Simon Hudon (Jun 29 2020 at 14:42):

I hope it was still an interesting challenge

view this post on Zulip Manuel Eberl (Jun 30 2020 at 13:55):

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.

view this post on Zulip Manuel Eberl (Jun 30 2020 at 14:05):

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.

view this post on Zulip Reid Barton (Jun 30 2020 at 14:14):

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.

view this post on Zulip Reid Barton (Jun 30 2020 at 14:16):

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.

view this post on Zulip Reid Barton (Jun 30 2020 at 14:16):

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.

view this post on Zulip Reid Barton (Jun 30 2020 at 14:20):

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

view this post on Zulip maximilian p.l. haslbeck (Jun 30 2020 at 14:21):

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!

view this post on Zulip maximilian p.l. haslbeck (Jun 30 2020 at 14:24):

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.

view this post on Zulip maximilian p.l. haslbeck (Jun 30 2020 at 14:28):

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.

view this post on Zulip maximilian p.l. haslbeck (Jun 30 2020 at 14:29):

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

view this post on Zulip maximilian p.l. haslbeck (Jun 30 2020 at 14:31):

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?

view this post on Zulip Mario Carneiro (Jun 30 2020 at 15:01):

I'm willing to volunteer to review the problem statements


Last updated: May 11 2021 at 22:14 UTC