alt Hacker News> If this file is correct and Lean kernel is correct, the proof is correct
There are two ifs in this sentence.
Replies
dev_dan_2 • yesterday at 5:09 PM
What is your point? Please don't be obtuse, it is more constructive to make your points clearly.
> If this file is correct and Lean kernel is correct, the proof is correct
There are two ifs in this sentence.
What is your point? Please don't be obtuse, it is more constructive to make your points clearly.
What is your point, exactly? Increasing number of people working in and around mathematics are relying on Lean kernel's correctness. That's kind of the point of tools like Lean. Why is it a problem for me to publish a result that relies on it? How do you think other Lean proofs work?