> energy to assess the correctness and relevance of such "results".
The author claims to have a proof in Lean. Checking the correctness of the result is now reduced to checking the definition of the constant.
The author claims to have a proof in Lean. Checking the correctness of the result is now reduced to checking the definition of the constant.
But this doesn't mean the remaining task is small or doesn't ask much from the reviewer, does it?! Otherwise we'd see a considerable turn-out of new findings on https://palomar-registry.org/ or https://github.com/Vilin97/lean-pool , or not?! (A considerable number of the presented proofs claim new results, as far as I can tell.)