Login
You're viewing the discuss.systems public feed.
  • abadidea0xabad1dea@infosec.exchange
    Jul 29, 2026, 7:34 AM

    Okay, we have a new contender for Most AI Thing to Ever Happen

    1) July 25th: someone messes around with an LLM and posts a proof of the Collatz conjecture that does, in fact, verify in the theorem prover. (The AI use is not disclosed on the github page) github.com/xrchz/CollatzLean

    2) July 26th: several serious bugs are posted in the theorem provers, that in principle could allow a false statement to be "proven" true. They're serious, yes, but no need for panic, because you're not going to blunder into accidentally exploiting the bugs while writing a proof, probably.
    github.com/leanprover/lean-ker

    3) July 28th: someone who was right to be very skeptical of the Collatz proof, and had the expertise to study it with a fine-toothed comb, discovered it was exploiting a bug github.com/leanprover/lean4/is

    4) The "proof" turns out to be exploiting multiple similar but distinct bugs to pass different solver variants!

    ⚠️⚠️[IMPORTANT EDIT: it was later clarified that the person who originally posted the proof was already aware that it was buggy, and chose not to be clear about this up front, as a humorous way to file a bug. It's pretty clear from the discussion threads that plenty of qualified people did not immediately realize it was meant to be a bug report.]⚠️⚠️

    5) the human who posted the proof acknowledges the AI use and claims they did not knowingly point it towards the bugs it exploited. leanprover.zulipchat.com/#narr

    Note that the proof was posted shortly before the related bug reports were posted. It is an open question if the AI found people discussing the bugs shortly before they were formally posted and "decided" to exploit them, if the AI "knew about it" as a learned strategy from the training stage (putting every single "proof" it's ever made and ever will make into profound doubt), or if it's recently been repeatedly blundering into it by sheer stupidity and that's how people noticed the bug at about the same time.

    Theorem provers aren't magic, and have bugs just like all other programs. They are tools to help us double-check our reasoning. When you skip the reasoning and ask an AI to "prove" something for you that's over your head, you're entering an adversarial pact with the monkey-pawed Devil of Customer Satisfaction.

    my initial source for investigating this myself: lipn.info/@mevenlennonbertrand

    💬 26🔄 669⭐ 893

Replies

  • Mariomario@don.tbully.me
    Jul 29, 2026, 7:37 AM
    @0xabad1dea > Theorem provers aren't magic, and have bugs just like all other programs.
    but what about metarocq? :blobcatopenmouth:
    if you have a fully-verified toolchain to evaluate the proof then the theorem prover should be proven to be correct
    💬 3🔄 0⭐ 0
  • 💬 0🔄 1⭐ 8
  • 💬 0🔄 0⭐ 1
  • 💬 0🔄 0⭐ 0
  • abadidea0xabad1dea@infosec.exchange
    Jul 29, 2026, 10:08 AM

    @mario @shelldozer it very well may be the most formally correct piece of software we've ever produced, but keep in mind it still has to run on a physical computer it's sharing with less-verified software and is also vulnerable to things like Rowhammer-class ram corruption attacks if one wants to intentionally manipulate it.

    There's no final escape hatch beyond which a computer can be absolutely guaranteed to always compute the correct answer, especially when someone has a vested interest in getting it to output the wrong answer.

    💬 2🔄 1⭐ 13
  • Mariomario@don.tbully.me
    Jul 29, 2026, 10:10 AM
    @0xabad1dea @shelldozer ~but that's not a bug anymore, that is a hardware issue. my scope was correct software.~
    i'm tired, sorry :ablobcatmelt:
    i believe there is a way to archive perfect software, be it in a very limited environment.
    💬 0🔄 0⭐ 0
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 11:01 AM

    @mario @0xabad1dea @shelldozer right, that's not a bug in software

    so, you can say the following isn't true for metarocq
    > Theorem provers aren't magic, and have bugs just like all other programs.

    but having the probability of hardware issues still makes the following true
    > Theorem provers aren't magic

    💬 1🔄 0⭐ 1
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 11:04 AM

    @mario @0xabad1dea @shelldozer not to say, they aren't magic, like i love theorem provers, and they are in a way very magical pieces of software humans have come up with

    all this means is they shouldn't become the single source of truth

    💬 1🔄 1⭐ 4
  • Mariomario@don.tbully.me
    Jul 29, 2026, 11:09 AM
    @calx @0xabad1dea @shelldozer but they actually aren't magic :blobcat3c:
    especially isabelle and rocq are actually somewhat easy to break down to their theoretic basics. they are very good tools to learn about proof theory.
    💬 2🔄 0⭐ 0
  • 💬 0🔄 2⭐ 7
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 3
  • Mariomario@don.tbully.me
    Jul 29, 2026, 5:20 PM
    @crazazy @0xabad1dea @calx @shelldozer @mansr
    > limits
    depends on the logic at hand. like first-order logic is complete and afaik solved within less than 200 characters of prolog
    peano is incomplete, but here are other arithmetics that are complete like presburger that is complete.
    💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 1
  • Haelwenn /элвэн/ :triskell:lanodan@queer.hacktivis.me
    Jul 31, 2026, 7:30 PM
    @0xabad1dea @mario @shelldozer Yeah, although couldn't that be minimised a lot by running the checks on different kinds of hardware and underlying implementations? (Given portable enough code)

    Also coming from a more "trusting trust" point-of-view, quite glad they note that proving Coq in Coq itself has quite few problems.
    💬 0🔄 0⭐ 0
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 10:56 AM

    @mario @0xabad1dea the hardware can be faulty too, tho. no? and we can have a bit flip error, tho that can be avoided by checking multiple times

    edit: it was already mentioned, my bad

    💬 0🔄 0⭐ 1
  • 💬 1🔄 0⭐ 0
  • David Chisnall (*Now with 50% more sarcasm!*)david_chisnall@infosec.exchange
    Jul 29, 2026, 1:28 PM

    @mario @0xabad1dea @calx

    Verification is only as good as the models and the properties you verify.

    My favourite example of this was a verified Arm core, which had dataflow proofs of all of its TrustZone implementation. This was then laid out for the back end in such a way that the wire that carried the TrustZone state went very close to another wire. Running the right sequence of instructions would induce a current and toggle from NS to S state, allowing unprivileged instructions to jump to secure mode (the layout was done as a research demonstration, not something in real production).

    So even the security properties that were formally verified on the RTL were not actually present in the physical silicon.

    💬 1🔄 10⭐ 53
  • Mariomario@don.tbully.me
    Jul 29, 2026, 1:51 PM
    @david_chisnall @0xabad1dea @calx > the models and the properties
    that is outside the scope of a theorem prover. if you prove properties of an invalid spec you have shown the implementation to be correctly invalid.
    💬 1🔄 0⭐ 0
  • 💬 1🔄 3⭐ 18
  • Mariomario@don.tbully.me
    Jul 29, 2026, 1:55 PM
    @david_chisnall was there any proof that the relevant properties of the abstract machine and the concrete machine were equivalent? :blobcatopenmouth:
    💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 2
  • 💬 0🔄 0⭐ 0
  • David Chisnall (*Now with 50% more sarcasm!*)david_chisnall@infosec.exchange
    Jul 29, 2026, 2:10 PM

    @mario There is some really exciting work to try to prove equivalence between the various layers of lowering from RTL to silicon, but it's very early. It's basically a full abstraction proof and those are hard enough even when you don't have 'physics' as one of the layers.

    💬 0🔄 1⭐ 5
  • derptroncrazyeddie@mastodon.social
    Jul 29, 2026, 2:26 PM

    @mario @david_chisnall In certified software development--the ones I was involved with and read about anyway--this is done by a person who signs off that the implementation follows the spec correctly. There's a bunch of this sort of thing that happens before any silicon is made. Takes a long time and is thus very expensive.

    Described situation was a demo during research phase sounds like. I hope they'd have found this before it made to production but yeah, no guarantees.

    💬 1🔄 0⭐ 1
  • David Chisnall (*Now with 50% more sarcasm!*)david_chisnall@infosec.exchange
    Jul 29, 2026, 2:34 PM

    @crazyeddie @mario

    In certified software development--the ones I was involved with and read about anyway--this is done by a person who signs off that the implementation follows the spec correctly.

    No it isn't. At no point in certified software development will anyone sign of on (for example) the C compiler's output being a 100% faithful representation of the C abstract machine. At least, not in any situation where liability may lead back to them, because it is never true (well, it's technically true for CompCERT, though with the all-bets-are-off-if-your-source-code-has-any-undefined-behaviour get-out-of-jail-free card).

    Described situation was a demo during research phase sounds like. I hope they'd have found this before it made to production but yeah, no guarantees.

    No, the point of the demo was that you would not find this. It was a tweak that was possible to make during back-end layout or to the GDSII after you've sent it to the fab, so a completely plausible supply-chain attack on a hardware security mechanism.

    This kind of attack is easier on hardware than software, because you can at least run a compiled program on a simulator.

    💬 1🔄 0⭐ 4
  • derptroncrazyeddie@mastodon.social
    Jul 29, 2026, 2:35 PM

    @david_chisnall @mario "At no point in certified software development will anyone sign of on (for example) the C compiler's output being a 100% faithful representation of the C abstract machine."

    This is quite the straw man you've summoned. Didn't get any better either.

    Later.

    💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 1
  • 💬 1🔄 0⭐ 0
  • David Chisnall (*Now with 50% more sarcasm!*)david_chisnall@infosec.exchange
    Jul 29, 2026, 2:38 PM

    @crazyeddie @mario

    I can only assume you're not reading the thread in context because you jumped into a middle of a conversation with a post about a problem with the concrete machine not being a faithful representation of the abstract machine that the proofs were constructed in to say that, in certified software development, people signed off on that.

    💬 0🔄 0⭐ 1
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 2:07 PM

    @mario @0xabad1dea @david_chisnall i can't seem to agree with this take, i am probably super wrong, but

    i'll define a theorem prover as something that, when provided with a proof, can say with 100% surety whether the proof contains any mistake or not, and thus if it is valid, according to current database of proven methods

    and if you agree with my definition, that should also include anything that isn't directly a part of the theorem prover, but still impact how it's output gets interpreted by the human, including,
    - the software,
    - the formal proof for that software,
    - the hardware,
    - the formal proof for that hardware,
    - the model of the hardware, and
    - even the human brain interpreting the results,

    without having a 100% surety on all these terms, we can't say that, when theorem prover verifies a proof, the proof is true, with 100% surety.

    💬 1🔄 0⭐ 1
  • Mariomario@don.tbully.me
    Jul 29, 2026, 2:16 PM
    @calx @0xabad1dea @david_chisnall a proof is only valid within it's system. in the case of rocq the system is the calculus of inductive constructions i.e.
    there are extraction systems which translate the formal language of rocq (gallina) into high-level code like ocaml or c.
    these are two different structures, like you have the formal logic side and you have the computation side which are connected via the curry howard correspondence.
    like a theorem prover assists you by providing tools for theorem proving, it's scope is formal logic.
    💬 1🔄 0⭐ 0
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 3:22 PM

    @mario @0xabad1dea @david_chisnall this kinda is making sense to me
    basically, what i think you mean is

    when we say "this proof is verified by xyz verifier", all the uncertainty that i mention gets put under the assumption that verifier isn't faulty

    right?

    i was going over whether that assumption can be true in my post, and what you're saying is once we add that assumption to our system, the proof becomes valid in that system, right?

    💬 1🔄 0⭐ 0
  • Mariomario@don.tbully.me
    Jul 29, 2026, 3:29 PM
    @calx @0xabad1dea @david_chisnall > once we add that assumption to our system, the proof becomes valid in that system, right?
    if you are able to prove that assumption within your knowledge space and tactics then it already was part of the system in the first place. but now you don't only have proven that assumption in your system but you have also found an instance of the assumption you can then further use in proving more stuff. at least for constructive logic thats the case.

    > the assumption that verifier isn't faulty
    that can be proven actually
    💬 1🔄 0⭐ 0
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 3:39 PM

    @mario @0xabad1dea @david_chisnall
    > > the assumption that verifier isn't faulty
    > that can be proven actually

    but to remove that assumption and to prove it, you'll need to add some other assumption, maybe about the hardware you'll use to prove the previous assumption, or maybe the model modelling the system on which the theorem prover will run

    in no way can a theorem prover, escape from its dependence on the assumptions about the system it is running on

    a normal proof doesn't have any such hidden dependence

    💬 0🔄 0⭐ 1
  • 💬 0🔄 0⭐ 0
  • 💬 1🔄 1⭐ 8
  • 💬 0🔄 0⭐ 4
  • 💬 1🔄 3⭐ 14
  • Dandijumx@mstdn.social
    Jul 29, 2026, 9:23 AM

    @whitequark @0xabad1dea Many years ago, while I was at Uni, one of the PhD students told me of a machine learning system that could design circuits and a human would build it on a test bed.

    One time, they tried to get it to generate something involving an oscillator. The solution it came up with was a single wire. It worked, but they didn't know why.

    They tracked the "bug" down to the fact the system had exploited the 50Hz RFI from the mains.

    💬 3🔄 2⭐ 26
  • 💬 2🔄 0⭐ 1
  • abadidea0xabad1dea@infosec.exchange
    Jul 29, 2026, 9:28 AM

    @whitequark @dijumx there's also been anecdotal reports of evolved circuits that work perfectly until you remove them from the specific table they were assembled on

    💬 2🔄 1⭐ 16
  • ✧✦Catherine✦✧whitequark@treehouse.systems
    Jul 29, 2026, 9:30 AM

    @0xabad1dea @dijumx yeah, that's pretty normal, what's unclear to me is what kind of model includes 50 Hz EMI (assuming one-shot design) and how it is simulated. if it iteratively removed a bunch of stuff until just a wire remained i can see that though

    💬 1🔄 2⭐ 3
  • 💬 0🔄 0⭐ 0
  • aoanlaaoanla@hachyderm.io
    Jul 29, 2026, 8:00 PM

    @0xabad1dea @whitequark @dijumx yeah, I've said to multiple people that "LLM coding" and "LLM mathsing" all remind me strongly of the 1990s-2000s evolutionary programming / algorithms / circuits stuff, where you get inexplicable results that absolutely *minimise the cost function* but probably not *how you actually intended* or *in a way that is useful generally*

    💬 0🔄 0⭐ 1
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • Dandijumx@mstdn.social
    Jul 29, 2026, 9:35 AM

    @whitequark @0xabad1dea I was at the University of Reading. Can't remember where this system was though, certainly wasn't one of ours; just something one of the PhD students knew about, and used as an example to explain how machine learning (and optimisation systems) can find the weirdest loopholes.

    💬 1🔄 0⭐ 3
  • 💬 0🔄 1⭐ 0
  • ✧✦Catherine✦✧whitequark@treehouse.systems
    Jul 29, 2026, 12:55 PM

    @dragonfi @dijumx @0xabad1dea it's really not hard at all to induce FPGA LUTs to interact via parasitic oscillator lock-in, by the way: lab.whitequark.org/notes/2016-

    people treat it as some magic miracle when an evolved circuit does that. it's not. doing weird nasal demon things is literally the default. and leveraging weird nasal demon things to manipulate a fitness function is the entire purpose of an ML algorithm anyway

    💬 1🔄 2⭐ 6
  • Evelyn Estelledragonfi@social.jsteuernagel.de
    Jul 29, 2026, 6:32 PM

    @whitequark @dijumx @0xabad1dea

    I agree, but it still feels like a "magic miracle" when statistics predicts the most likely outcome and it indeed comes true, but following the exact chain of causality is an exercise in frustration. Physics is full of phenomena like that.

    💬 0🔄 0⭐ 1
  • Justin DerrickJustinDerrick@mstdn.ca
    Jul 29, 2026, 10:27 AM

    @dijumx @whitequark @0xabad1dea I vaguely remember something similar where someone was testing “genetic” programming - starting with a simple goal, then altering the code (a new ‘generation’) that ran on an FPGA, and running it as a test. The goal in this case was to reliably detect a specific sound or radio transmission.

    After it got up and running, it took a couple thousand iterations, but it had developed a working set of instructions.

    When reviewed, the code was awful, and had large blocks of code that did essentially nothing.

    When the blocks of nothing were removed, it stopped working. When they were re-added, it worked again.

    When the FPGA was replaced with an identical board, it ALSO stopped working.

    The process had found and exploited some property of that specific FPGA chip to achieve its goal, but the end result couldn’t be used because it couldn’t be understood or replicated.

    💬 2🔄 1⭐ 5
  • 💬 0🔄 1⭐ 4
  • ShadSterlingShadSterling@mastodon.social
    Jul 29, 2026, 1:11 PM

    @JustinDerrick @dijumx @whitequark @0xabad1dea the variant I read about maybe a decade ago was one where the FPGA layout had loops, not connected to the input or the output, but breaking the loop would make it fail. IIRC the authors suspected it was relying on some weak analog interference but confirming that was out of scope. I don’t think the evolving algorithm is a nasal demon tho, because it isn’t intended to find reusable results

    💬 1🔄 1⭐ 3
  • 💬 0🔄 0⭐ 0
  • 💬 1🔄 0⭐ 1
  • 💬 0🔄 0⭐ 0
  • P4p4@masto.ai
    Jul 29, 2026, 6:59 PM

    @dijumx @whitequark @0xabad1dea years ago I stumbled on a big-ass spreadsheet full of examples where systems tasked with a problem find an "optimal" solution by finding exploits.

    I remember most of it being artificial life simulators where the creatures evolved to abuse the rules of the simulation or breaking the physics, but there were a few examples of exploiting real-world imperfections too.

    Whish I could find it again.

    💬 0🔄 0⭐ 1
  • 💬 1🔄 3⭐ 11
  • Meven Lennon-Bertrandmevenlennonbertrand@lipn.info
    Jul 29, 2026, 8:13 AM

    @mattblaze @0xabad1dea I think it's practically ok, we have good human measures in place to avoid such bugs having serious consequences. Of course, on the long run this is a strong motivation to apply serious formal methods to proof assistant kernels, ideally towards full verification!

    💬 1🔄 0⭐ 4