Technology

88,825 readers

14,656 active

3,514 users here now

This is a most excellent place for technology news and articles.

Our Rules

Follow the lemmy.world rules.
Only tech related news or articles.
Be excellent to each other!
Mod approved content bots can post up to 10 articles per day.
Threads asking for personal tech support may be deleted.
Politics threads may be removed.
No memes allowed as posts, OK to post as comments.
Only approved bots from the list below, this includes using AI responses and summaries. To ask if your bot can be added please contact a mod.
Check for duplicates before posting, duplicates may be removed
Accounts 7 days and younger will have their posts automatically removed.

founded 3 years ago

moderators

submitted 1 week ago by Mustachius_Grumpius@thelemmy.club to c/technology@lemmy.world

you are viewing a single comment's thread
view the rest of the comments

[–] FauxLiving@lemmy.world 15 points 1 week ago (1 child)

The proofs are written in Lean so, like in all mathematics, you don't have to trust the person because you can independently verify the proof.

parent

[–] ThirdConsul@lemmy.zip 4 points 1 week ago

That's not how Lean works.

implementation of Lean is buggy.
having a Lean Theorem/Proof only proves they are connected to the axioms
Lean is not enough to personally verify the proof. We can see that even now with the stolen C+D Navier proof, where OpenAi paper - as we know since yesterday - is... possibly false (well, we know that the lean code does not match the paper, let the mathematicians cook).

parent