alt Hacker News> forcing the mathematicians community to do the verification job for them
What do you mean? They're publishing the Lean proofs themselves. Who's forced into anything?
> forcing the mathematicians community to do the verification job for them
What do you mean? They're publishing the Lean proofs themselves. Who's forced into anything?
They are not publishing Lean proofs. They are publishing proofs in natural language, and are not submitting to journals.
They are just putting out a bunch of weirdly written extremely long and technical papers and saying: Hey, here is the solution (we hope there are no mistakes).