4
\$\begingroup\$

Lean is now the Language of the Month. Yay!

But... Lean is a theorem proving language. It is also a general purpose, Turing complete1 programming language too but I mean... Lean isn't exactly better than other languages on that front wrt code golf.

On the Lean Zulip chat, sometimes users compete to write the shortest proof possible for a given lemma. Could we also do something similar on this Code Golf website?

The main issue with this is that this wouldn't be language agnostic: how the problem statement is formalized, or specified in the theorem proving language can significantly affect the proof.

1 You can turn off the termination checker. There are functions to interact with the operating system.
\$\endgroup\$
1

1 Answer 1

Reset to default
4
\$\begingroup\$

We generally want challenges to be open to all languages. However when you have a good reason restrict a challenge to a particular language you should.

When it comes to "What is the shortest way to prove this theorem?", I don't think there is a good way to express that idea in a language agnostic way, and it seems like you are struggling with the same thing.

So don't worry.

I've asked language specific challenges in the past this way and they don't seem to be particularly damaged by this fact.[1][2][3] I do think that any of these challenges would be significantly worsened by attempts to make them language agnostic. They would have to be very complex in their definitions, making a bloated challenge that's only really fun in one or two languages anyway.

Right now Lean is the LotM, so I think that there will be some amount of interest in Lean and it's features. I was even planning on asking a question like the one you describe sometime this month.

\$\endgroup\$
2
  • 2
    \$\begingroup\$ Reading this and thinking a lot about it, I agree that the best way to pose a "proof" code golf is to restrict it to a single language. While a target theorem could be stated in a language-agnostic way theoretically, there are potentially many ways to express it in a given language, with massively different results in code golf, and it would be extremely hard to establish fairness across theorem proving languages (with different underlying theory and different stdlib, etc). \$\endgroup\$
    – Bubbler
    Oct 4, 2021 at 4:43
  • \$\begingroup\$ @Bubbler Lengths of formal proofs are well-defined in logic and independent of programming languages. They depend on specific calculi, i.e. sets of axioms and rules of inference, e.g. see this example. The issue with provers like Lean is that you have a general language that can describe all kinds of calculi, so that "proof length in Lean" is not actually a thing since using the theorem as an axiom always yields a proof of length 1. One confusingly using such words would probably mean "the length of code in a specific language to prove something". \$\endgroup\$
    – xamid
    Nov 24 at 22:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .