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.

Missing information is different from paying the person who steals information instead of paying the person that produces it. Did you bother to think critically before you replied, or is an AI doing all your thinking as well?

So you'd rather give money to the company that stole the copyrighted material of experts and academics instead of giving them money? Sure some textbooks are corporate greed schemes themselves, but many others are just the work of a group of professors

You mean that technology that resulted in a massive bubble, wasn't marketed as replacing all labor and giving the rich personal slaves? You mean the technology that enables human communication and creativity instead of promoting human isolation and stealing human creativity?

Horseshit. ~30% of US citizens are happy with this state of affairs. ~30% are completely disengaged, believe ridiculous things like "both sides are the same" or feel like politics doesn't effect them. ~30% voted for Harris, Biden, and Clinton before that.

The software is heavily regulated for medical devices. Saying an MRI machine has bad software seems highly unlikely to me. This is of course different from Epic, but even then as a patient MyChart is really not that bad

Don't bother, Republicans are the only ones that care about the debt and their ideology makes them incapable of realizing there very choice of candidates is the exact problem

This is not the argument. It's not a comparison to gambling but a comparison to something that does not materially improve a person's life. Economic expenditure does not equate to human benefit. This is the original argument, and the onus is on THAT person to explain why people spending for AI actually benefit, not the other way around.

Perhaps you can ask Claude to explain it to you.

Incorrect. The statement in Lean can itself be wrong. Moreover, they could be exploiting a kernel bug in Lean, of which we had one published literally a week ago.

What is absurd is evaluating something on the lines of code it produces. AI psychosis at work.

This is horseshit. Mathlib3 and mathlib4 all existed prior to LLMs. Unimath of Agda, mathematical components of Rocq, the list goes on.

LLMs have done nothing for "making large scale mechanization viable." They have been viable. The only thing has changed is the perception of the random developer who never wanted to put the effort into learning what actually needed to be learned and are instead happy to spit our complete garbage, spec and all, and say it's a proof of something.

It's not shocking at all that the people who seem to get any benefit out of LLMs in the proof assistant space are the ones who could have just don't it themselves anyway.

A basic course in statistics will inform you of why a 99.99% accurate test should be looked at with skepticism when diagnosing a rare disease. Yet we see the fancy 9s and think somehow this many 9s is enough.

Sure if you're a rich slave owner.

They would just choose a different domain name, it's not that important and the previous years tend to forward link anyway.

Researchers _would_ leave in droves if they could. But it turns out the entire world doesn't actually care much for research. The US was actually unique in that regard.

Comparing it to the trolley problem is incorrect. COVID had real potential to kill you, even as a young person. At that point its a matter of risk assessment for yourself. Take a 2% chance of dying, a slightly higher chance of reduced quality of life (long COVID), or take a lottery-winning chance of dying to this blood clot. It is appropriate to do the math correctly to decide if this makes sense, but to claim that scientists and advocates did not do this personal risk assessment math and merely went off the benefits of herd immunity is a lie and anti-vaccine propaganda.

Let's take a moment to put the AI psychosis down and think through your comment:

1. AI is so good that you can get your game working to your vision in a matter of weeks without needing to depend on godot

2. Godot is making a mistake refusing AI contributions

How exactly is godot making a mistake, if AI is so good that godot is defunct anyway?