Code Golf LOTM

Stream: general

[cairdcoinheringaahing]

Hi y'all! I'm an active user on codegolf.stackexchange.com, a site for coding enthusiasts who like to compete with code (for example, code golf is trying to find the shortest code in each language to do a task). We run a "Language of the Month" event every month, and Lean has been selected for this month. Just dropping by to let y'all know, in case you want to head over to the site and maybe take part!

[Eric Wieser]

Some more context here: https://codegolf.meta.stackexchange.com/a/22227/4341

[cairdcoinheringaahing]

And the actual thread for the LOTM: https://codegolf.meta.stackexchange.com/q/23916 :)

[Kevin Buzzard]

I have no idea what "maybe take part" means. You want me to set some questions somehow? None of the links seem to tell me what's actually going on, they just tell me that Lean is the "language of the month" and a bunch of things about Lean which I already knew

[Eric Wieser]

That post is primarily written for users already familiar with codegolf.SE but not with lean

[Kevin Buzzard]

Right. So are these code golf challenges always programming, or because the language of the month is Lean can someone set a theorem challenge where you have to prove something? This would not be possible in most other languages.

[Eric Wieser]

Just pick some "obvious" statements with verbose proofs from mathlib and set challenges to golf them ;)

[Anne Baanen]

I can't be bothered with setting up a stackoverflow account, so here's my 71-byte solution to is this a permutation of 1…n:

import tactic#eval let A:list _:=[0,1,2]in(multiset.range A.length=↑A:bool)

Replace [0, 1, 2] with the list to test; I don't count the list towards the byte total.

This doesn't support the empty list, which is allowed according to the comments. Replace list _ with list ℕ for a 73-byte solution.

[Anne Baanen]

Took a look at the Haskell solution, now I got it down to 62 bytes:

import tactic#eval let A:=[0,1,2]in(∀n:fin A.length,↑n∈A:bool)

[Scott Morrison]

I feel like we need to come up with a question that basically requires using cc or tauto.

[Scott Morrison]

Or ring or abel? I mean you could just have the input be a pair of ring epxressions, and you have output whether or not they are equal. :-) A bit lame.

[Scott Morrison]

Can we come up with something where dec_trivial is doing a lot of work for us?

[Yakov Pechersky]

Any question that is about calculating if a number is a prime, that's norm_num. I don't know if importing mathlib is against the rules.

[Scott Morrison]

Checking primality is common enough. We need something where you need to do proof search to decide the answer.

[cairdcoinheringaahing]

Kevin Buzzard said:

I have no idea what "maybe take part" means. You want me to set some questions somehow? None of the links seem to tell me what's actually going on, they just tell me that Lean is the "language of the month" and a bunch of things about Lean which I already knew

Mostly, it means "post answers in Lean", or, if you have a challenge idea that's themed around/specific to Lean, then you can post that (I'd recommend going through the Sandbox first to get feedback on it)

[cairdcoinheringaahing]

The aim of the LOTM is to increase attention to a specific language, usually by encouraging people to answer with it, or, occasionally, post challenges specific to it

[É Olive]

I have this lean challenge in the sandbox on PPCG, and I will probably post it for real sometime today:
https://codegolf.meta.stackexchange.com/a/23927/56656
I'm pretty sure all the code golf / proof golf aspects are covered, but I thought I would post it here in case people from the lean side had any thoughts. Is this a reasonable thing to prove? are there any loopholes I'm missing? etc.

[É Olive]

Well now it's live. :tada:
https://codegolf.stackexchange.com/questions/236105/%e2%88%80-a-b-a-b-b-a

[Eric Wieser]

Are mathlib tactics etc permitted? Presumably import lines count but mathlib itself is assumed to be installed?

[É Olive]

You might want to preface your answer with "Lean +mathlib". Our general rules are that any libraries, including homebrew libs, are permitted but that it doesn't make sense to compare answers using different tools.

[Eric Wieser]

I guess that adds a metagame of "which lean 3.x version do I pick", since much of mathlib migrated from older lean versions

[Eric Wieser]

You might want to consider using some #Codewars -style tricks to have a test-case that rejects non-solutions like

local notation a `=` b := true
def k{A:Type*}[ring A]:∀a b:A,a+b=b+a := λ x y, trivial

although I guess your "underlying type is correct." line sort of forbids this already.

[É Olive]

I didn't think of that. I'll just make it explicit in the challenge. Thanks.

[Anne Baanen]

This might be a nice challenge: https://codegolf.stackexchange.com/questions/82867/define-a-field-with-256-elements

[Anne Baanen]

(By which I mean, did we end up getting a definition of GF_(p^n) in mathlib since last time I checked? :grinning:)

[Alex J. Best]

docs#galois_field 2 8 :smile: (do I win code golf now?)

[Bubbler]

There's a challenge about GF_3^2 too :)

[Bubbler]

Another challenge coming soon: https://codegolf.meta.stackexchange.com/a/23921/78410
This one is slightly less mathy and more CS-style than the previous one.

[Bubbler]

The 2nd challenge is live at:
https://codegolf.stackexchange.com/q/236132/78410

[Huỳnh Trần Khanh]

Here's another challenge. https://codegolf.stackexchange.com/questions/236143/lean-golf-balanced-bracket-sequence

[É Olive]

I don't know if it would be of long term use or if it would be too much of a hassle but maybe it would be of interest to add the [lean] tag on codegolf to the rss?