Is there a way to say "find X" in lean?

Stream: general

[Wang Jingting]

I was watching the video on youtube in which David Silver said something about Alphaproof just now, and as he mentioned, there are lots of mathematical problems stated as "find X" rather than proving something. So I began to wonder how we could state similar things formally. I understand that "find X" itself might not have been a very rigorous mathematical concept, people tend to have different opinions on what can be an answer to that. (like if the problem is determining a set of natural numbers, then {x : Nat | Even x} might be considered an answer, but simply rephrasing the problem as the desription of the set would certainly not be considered an answer) But I'm still curious on how we could possibly state problems like these in lean in some way, or how could this be facilitated in lean?

[Wang Jingting]

(The video was from 4 months ago at the second half of video, I came across the link of it in zulip)

[Wang Jingting]

I think perhaps it will have something to do with computability? Like, if we go from {x : Nat | P x} to {x : Nat | Q x}, where P is not computable but Q is, then that's certainly considered a progress.

[Robert Maxton]

This is basically the heart of the Curry-Howard isomorphism to begin with! Proving a statement amounts to finding a value of a given type; precisely what counts as "finding a value" depends primarily on the strength of your axiom of choice (or whether you accept it at all)

[Robert Maxton]

Simply describing a set or nonconstructively proving that one exists is only valid with choice; excluding choice entirely is how you force actually producing a concrete description

[Luigi Massacci]

Wang Jingting said:

I was watching the video on youtube in which David Silver said something about Alphaproof just now, and as he mentioned, there are lots of mathematical problems stated as "find X" rather than proving something. So I began to wonder how we could state similar things formally. I understand that "find X" itself might not have been a very rigorous mathematical concept, people tend to have different opinions on what can be an answer to that. (like if the problem is determining a set of natural numbers, then {x : Nat | Even x} might be considered an answer, but simply rephrasing the problem as the desription of the set would certainly not be considered an answer) But I'm still curious on how we could possibly state problems like these in lean in some way, or how could this be facilitated in lean?

you can wait for the AlphaProof paper to come out and it will presumably specify how that was achieved. More generally, if you look here on zulip in threads discussing formalisation of olympiad problems, many approaches have been discussed

[Luigi Massacci]

(and more or less all boil down to metaprogramming, rather than philosophy ; )

[Eric Wieser]

Wang Jingting said:

then {x : Nat | Even x} might be considered an answer, but simply rephrasing the problem as the description of the set would certainly not be considered an answer)

This problem is not unique to formal math; when setting problems for students, this kind of answer would surely be undeserving of marks. Similarly, there are answers that sit half way between the tautology and the desired result, for which a grader would likely award only partial credit

[Jeremy Avigad]

As I understand it, the AlphaProof approach was to train one model to guess a theorem that would count as a legitimate answer and then use another model to try to prove it. That's clearly wasteful, though, because when a guess fails, no information is carried over to the next attempt. I had fun discussing this Alex Davies, Amaury Hyatt, and Melanie Matchett Wood at the Harvard CMSA a few months ago:
https://www.youtube.com/watch?v=_KjtUUKOITs
But I am sure DeepMind and others are doing more sophisticated things now.

[Joseph Myers]

I'd guess that the information is carried over to attempts to prove or disprove other guesses (via the test-time RL, supposing that works across different guesses not just across mutated problem variants). But maybe not to attempts to produce new guesses. (I've wondered how AlphaProof would do on problems such as 2013 shortlist A5 with an unlikely looking answer that would be hard to guess without feedback to the guessing process from proof attempts.)

[Thomas Zhu]

This topic has been discussed before here and here (and probably more places).

Robert Maxton said:

Simply describing a set or nonconstructively proving that one exists is only valid with choice; excluding choice entirely is how you force actually producing a concrete description

This might work in theory, but IIRC in practice Mathlib has long ago decided to not actively avoid the axiom of choice, so you can't rely on whether something needs choice. (I am not an expert on this topic). For example anything involving equality of real numbers probably uses choice and is noncomputable (e.g. IMO 2024 P1).

[Luigi Massacci]

Equality of real numbers needing some kind choice principle is not really a philosophical choice of mathlib, but a mathematical fact. You cannot have it any other way

[Trebor Huang]

Choice is irrelevant here, as for example if I answer "what is 2+2?" with "the answer is 2+2", it definitely doesn't count as a legitimate answer. And no amount of removing non-constructive axioms can exclude this. In this regard, choice has nothing to do with "non-concrete" descriptions.