voxl

As the people who view this as denigrating and deminishing the work of real people are just as repulsed.

In this case it does. Describe any effective measure to pick a random sample from the interval and you will have cheated into choosing from the computable reals instead (of which there is a countable amount)

Rocq has had similar issues with AI finding soundness bugs, particularly in module code last I checked. Yet they don't even have half the resources of Lean. Rocq is nowhere close in my opinion. Though this is really like comparing how many 9s. If Lean is 99.9999% trustworthy, than Rocq is 99.99% trustworthy.

Isabelle/HOL is probably at similar footing to Lean because its kernel is so simple.

For the highlighted kernel (con-leche) , they postulate a set theory. Godel doesn't get involved because the proof is effectively saying Lean+ZFC entails Con(Lean), but even that isn't quite right, because the kernel doesn't include all the features of Lean. But even that isn't quite right, because they're actively modifying the kernel to be "simpler" to check.

It's a marketing post at the end of the day is what I'm trying to say. Regardless, Lean is probably the most trustworthy proof assistant on the planet at this point.

You think a project that bans LLM contributions completely can be replicated in spirit by those who welcome it?

You expect an arxiv only paper to be cited? Do you even know fuck all about scientific research? Do you think someone can slap "Foundations of" in an arxiv title and we are mandated to cite it?

Your claim is still rubissh, as you neglected to interact with the rest of my comment: economic utility does not necessitate all mathematical output directly contributes.

You redefine "forgot" to make it falsiable, but also neglect that you need to refute that some "forgotten" work didn't contribute to new work down the line.

You bemoan the cherry picked example and counter with an unfalsifiable claim. Certainly we have remembered much more math than Calculus, and much of it has been of practical use.

How can we hope to quantity the expenditure on math we've collectively forgotten? It's unknowable by definition. The only reasonable thing to do is to determine the value added after the expense paid. Even in a world where calculus is the only thing that we took away from the math of 1700s my guess is that this is still an economically beneficial calculation.

Whataboutism. Two evils are still evil.

Probably yes. Only a handful of mathematicians work on this particular problem, and ALL of them do not exclusively work on this problem, while having administrative and teaching duties.

The real issue is we'll never know. The rich are willing to risk it all on charismatic CEO psychopaths but not on humans.

No you see people that use AI generally don't bother to consider this unimportant detail. Or they ask the AI to "double check" its work.

??? Look at any conference that publishes mechanized results? You'll see plenty of Isabelle, ACL2, Rocq, Agda. You exist in the pop science bubble. If Lean has done anything it's advertised itself well. It did a good job of that as far back as the Liquid Tensor Experiment, and it's pissed many people off in the community with it's marketing antics.

It's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another modest increase in trust, but to pretend the implementation of HOL-light has never had bugs and it's kernel could never have a bug is hubris.

Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.