They can't keep getting away with this.
>Twitter screenshot threadKill yourself retard
>>17078555so ai spits out a proof and we are supposed to trust it because humans can tweak it within lean_zfc? What if zfc is inconsistent? Doesn't the hack and their further twisting of it also become invalidated?
>>17078570based
>>17078570It doesn't matter. Keep fighting the good fight.
>>17078555So how many microseconds do I save per trillion integer multiplications?
>>17078570It would accelerate finding the flaws in zfc, of which there are numerous.
>>17078570>What if zfc is inconsistent? that never stopped miggers
>>17078570Why are mentally ill retards so obsessed with ZFC and keep bringing it up randomly and out of context?
>>17078914How do you think they constructed their lean statements?
>>17078922I don't know (and neither do you) but what the fuck would they need ZFC for, you absolute mong?
>>17078555they can and they will
>>17078928what else are they supposed to use?it's the only axiomatization that isn't completely bonkers
>>17078570>What if zfc is inconsistent? Then Lean is inconsistent too since it proves the consistency of ZFC. Contrary to some popular propaganda about type theory/category, neither Lean or Rocq (on which Lean is based) are "minimalistic", they both use some strong dependent type theory with universes.
>>17078564/thread
>>17079170Notice how you lack the metacognition to acknowledge that you have no idea why they would use ZFC so you just keep looping "b-b-b-but why wouldn't they?". The quickest way to get convinced that NPCs are real is to browse /sci/.
>>17079213I don't think you understood what point I was trying to makeand I'm not any of the niggers you've been talking toLean can in any case not prove its own consistency, if it is consistentnor does it only use ZFC, it uses an extended ZFC with n inaccessible cardinals for each natural number nwhich, you know... it's something?did you know that definitional equality is undecidable in Lean?>muh theorem checkinglmao
>>17079225You weren't actually making any point. Even if Lean turns out to be inconsistent, the chances of it invalidating a multiplication algorithm are negligible because you're not actually gonna be using ZFC, let alone anything more powerful than ZFC, for that.
>>17079226anything you do in Lean uses this extended ZFCdid you know that Lean does not implement equality, only "algorithmic equality" which is intransitive?
>>17079228>retard gets completely filtered by basic observations
All of these are even more useless than the O(n log n) one from 2019 which only worked with extremely large numbers. The result by OpenAI that started this whole trend only works on an inefficient Turing Machine which we will never use/emulate.
>>17078928On further review of lean deployments, the ZFC relationship to lean seems to be one way. So ZFC could justify lean but they are not isomorphic, etc.They did implement the axioms for the zfc corollary in lean in this case but that doesn't commute to the nature of the proof. It does undercut their autoformalism posture, but that wasn't what I was going for. My intent was even if their autoformalism is true, it is possible for their machine to not actually work in deployment. And this claim is not guaranteed so I have to retract it.
>>17079241>that doesn't commute to the nature of the proof.Isn't that the bottom line for any proof invokes only the principles of arithmetic?
>>17079170>what else are they supposed to use?ZF
>>17079265No, lean relies on type theory. This is isomorphic to logical argumentation. The autoformalism using a lean that is consistent with zfc is a red herring in this case. The undercutting is if it is pretended like it establishes something more about the lean system when it doesn't. It is exactly like an llm using lean in other instances, They were highlighting a version of lean they chose to use. When I was first looked at it, I thought it was mentioned as part of actually needing zfc machinery. It does not except in the unusual instance where someone for no reason wants to assert that the zfc consistency means the proofs are true or more likely to be true. It is using induction over types and those types just happen to be consistent with zfc. I think the intended signifier is that it isn't an exotic one off species from the llm.
>>17079170>>17079277Daily remainder that ZF and ZFC prove the same arithmetical sentences (like the one of OP) since such sentences are absolute for the constructible universe (a,y such P means the same thing inn the underlying universe U or in the L of U).You could freely use ZF or ZFC for the same such result.
>>17079379Lean does not use ZFC, or ZF
>>17078845name one
>>17079398>Lean does not use ZFC, or ZFLean proves the consistency of ZF (hence the consistency of ZF), which is even worse.
>>17079504> hence the consistency of ZFI mean ZFC of course
