This is what I suspected. Then would it be appropriate to create a new tag for this kind of challenge?

You mean a tag for the lean language? I guess so?

@user A tag for interactive theorem proving challenges.

Lean, Coq and Agda are interactive theorem proving languages.

But where do you draw the line?

One thing you could maybe do instead is use atomic-code-golf and restrict answers to some subset of lean and a special set of axioms

Idk if that’s how atomic golf is supposed to work tho

@user We should whitelist theorem proving languages that are known to be sound and widely used. If the community objects to this approach, maybe we should create a tag for Lean challenges specifically perhaps? On second thought, maybe a tag for Lean challenges would be better. Because the statement has to be formalized, or specified in the ITP language too.

Whitelisting interactive theorem proving langs doesn’t seem like the easiest thing to do, but it may be easier to differentiate between such a language and a language that isn’t one than other categories

Unless there’s a compelling reason to use Lean or Coq

I’d recommend bringing this up in tnb where more people will see it

@user Can you do that? I'm in a call unfortunately.

Thanks.

Nevermind. I'll do that myself.

TNB discussion

@HuỳnhTrầnKhanh Any ideas for challenges involving Lean?