## Stream: general

### Topic: Code Golf LOTM

#### cairdcoinheringaahing (Oct 02 2021 at 12:08):

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 (Oct 02 2021 at 12:14):

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

#### cairdcoinheringaahing (Oct 02 2021 at 12:15):

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

#### Kevin Buzzard (Oct 02 2021 at 14:24):

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 (Oct 02 2021 at 14:28):

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

#### Kevin Buzzard (Oct 02 2021 at 14:29):

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 (Oct 02 2021 at 14:30):

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

#### Anne Baanen (Oct 02 2021 at 22:33):

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 (Oct 02 2021 at 22:37):

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 (Oct 03 2021 at 00:36):

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

#### Scott Morrison (Oct 03 2021 at 00:38):

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 (Oct 03 2021 at 00:39):

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

#### Yakov Pechersky (Oct 03 2021 at 00:43):

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 (Oct 03 2021 at 00:46):

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

#### cairdcoinheringaahing (Oct 03 2021 at 12:44):

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 (Oct 03 2021 at 12:44):

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 (Oct 07 2021 at 08:50):

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 (Oct 07 2021 at 11:45):

https://codegolf.stackexchange.com/questions/236105/%e2%88%80-a-b-a-b-b-a

#### Eric Wieser (Oct 07 2021 at 12:15):

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

#### É Olive (Oct 07 2021 at 12:17):

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 (Oct 07 2021 at 12:36):

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 (Oct 07 2021 at 12:42):

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 (Oct 07 2021 at 12:45):

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

#### Anne Baanen (Oct 07 2021 at 12:46):

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

#### Anne Baanen (Oct 07 2021 at 12:48):

(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 (Oct 07 2021 at 12:51):

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

#### Bubbler (Oct 07 2021 at 12:52):

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

#### Bubbler (Oct 07 2021 at 12:58):

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 (Oct 08 2021 at 00:10):

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

#### Huỳnh Trần Khanh (Oct 08 2021 at 08:44):

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

#### É Olive (Oct 08 2021 at 13:15):

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?

Last updated: Dec 20 2023 at 11:08 UTC