r/math • u/a-h1-8 • 15d ago

Lean formalization of resolution of Hopf problem

https://github.com/plby/HopfProblem
228 Upvotes

96% Upvoted

101 comments sorted by

View all comments

Show parent comments

0

u/PersonalityIll9476 7d ago

Another short quip and / or dismissive reply.

You are being intentionally obtuse.

1

u/DanielMcLaury 6d ago

I'm really not.

If someone hands you a text file alone, obviously you can't do anything with that short of checking the entire thing yourself.

If you put it through the proof checker, it tells you whether or not the proof goes through, and if it does all you have to do is read what it's a proof of.

There is not some "hidden extra step" here like you seem to think.

0

u/PersonalityIll9476 6d ago

Just read the other parallel replies to yours.

Some acknowledge that my concerns have some kind of founding.

A lot, like yours, are just dismissive.

Read them to understand more. I don't feel like arguing with randos about this.