Why is this claimed to be proved in lean

Stream: mathlib4

[Matherian]

Since it contains "exact?", why is this clogged to be proved in lean? Thanks https://live.lean-lang.org/#project=mathlib-v4.24.0&url=https%3A%2F%2Fraw.githubusercontent.com%2Fplby%2Flean-proofs%2Frefs%2Fheads%2Fmain%2Fsrc%2Fv4.24.0%2FErdosProblems%2FErdos124.lean

[Matherian]

g/#project=mathlib-v4.24.0&url=https%3A%2F%2Fraw.githubusercontent.com%2Fplby%2Flean-proofs%2Frefs%2Fheads%2Fmain%2Fsrc%2Fv4.24.0%2FErdosProblems%2FErdos124.lean

[Weiyi Wang]

I don't know the context, but it does work if you apply the first suggestion from each exact?

[Weiyi Wang]

I think it means it is generally correct but needs clean up

[Weiyi Wang]

(same goes for all the non-terminal aesop and unused simp lemma)

[Ruben Van de Velde]

Yeah, it's not a proof as written (nor does it look like a particularly well-written proof), but each of the exact?s finds one of the other theorems in the same file

[Eric Rodriguez]

exact? does insert the correct term, even if it's not mathlib style to keep them as exact?

[Ruben Van de Velde]

Oh indeed, #print axioms does accept it. Still, not a reasonable proof

[Matherian]

Ruben Van de Velde said:

Yeah, it's not a proof as written (nor does it look like a particularly well-written proof), but each of the exact?s finds one of the other theorems in the same file

Ruben Van de Velde said:

Yeah, it's not a proof as written (nor does it look like a particularly well-written proof), but each of the exact?s finds one of the other theorems in the same file

Thank you for your reply. But if “each of the exact?s finds one of the other theorems in the same file,” then why shouldn’t a short line of code in the lean file refer to the theorem in the same file? Thanks.

[Kim Morrison]

@Matherian, do you understand how exact? works? You might need to research that first. :-)

[Matherian]

Kim Morrison said:

Matherian, do you understand how exact? works? You might need to research that first. :-)

Since there is a question mark, does it not mean it is undetermined, unconfirmed or unanswered?

[suhr]

Question mark means a question. And the tactic finds an answer (an expression that would prove the statement).

[Snir Broshi]

Matherian said:

Since there is a question mark, does it not mean it is undetermined, unconfirmed or unanswered?

The question mark is part of the name. The name implies what the tactic does, but it is only a name, there is no underlying meaning to the question mark.
There can be however a reason why the authors of the tactic chose to put a question mark there, and that reason is related to the adjectives you gave, but the reason for a name of a tactic has nothing to do with the proof itself.