whateverboat

There's a difference between a human trying to break into drug labs and changing experimental results vs a machine in that the machine can do it much easier today.

yes, hugely so.

Runtime robustness is all you need though.

The core of a proof checker is a formally validated core that is based on a small amount of concepts. Every single line in the proof reduces to that core, therefore, as long as you can trust the core, you can trust the execution of the proofs.

Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.

What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.

Developer Certificate of Origin

This is not a new problem. AI just changes the scale.

I didn't know their consumer cards had rocm.

VCS doesn't preserve your local history? Did we miss why git became successful? I mean I understand, you are not committing every 2 lines of code, so git is not replacement for persistent undo, but stil.

Life cycle of the fab is 3-5 years, an opimistic estimate of slow down in europe due to all the paper work is 2-3 years, so then you would rather not build the plant.

TSMC's Arizona fab needs 200MW of electricity.

But even more importantly, they need 2 separate completely independent substation feeds, since a 15 second interruption can cause 0.1B Euro of losses.

Finally, and here is where Europe really really suffers, generally you need these things to be planned, approved and built within a year.

This comment is one of the most bizzare things I've seen here regarding ArXiv.

No. You do have checks, it's just that once you publish 4-5 papers, 99% of your field is open to you so you never have to do the checks again.

weapons are a tool to wield political power.

It is quite well known that the culture around Pythagora's time was heavily influence by architecture and engineering like Tunnel of Eupalinos.

LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.

> Now that we can see their work, the approaches appear to be different. It is also worth noting that our latest model can solve many, many other math problems.

Is that a threat?