formal-verification

``` Taelin @VictorTaelin · 9m we're closer than you think > QUOTED: Zygi @nonagonono · 34m > Eventually we might get to a point where Lean proofs alone are adversarially robust. We're not there yet. But we're already close to (Lean proof typechecks & Claude/GPT reads and understands it) being adversarially robust. > QUOTED: Elliot Glazer @ElliotGlazer · 15h > Shoutouts to Ramana Kumar for refuting the Collatz Conjecture in Lean, *as checked by Comparator!* github.com/xrchz/CollatzL... [Embedded code block, Lean syntax, from a file appearing to define "Collatz.ProfileConstruction":] let currentNamespace ← getCurrNamespace let limitingName := currentNamespace ++ profileName let limitingType := mkApp (mkConst `Collatz.DescentProfile) stages.exceptionalParity let limitingValue := .letE `transferredEnvelope exceptionalEnvelopeType transferredEnvelope (.letE `stableEnvelope stableEnvelopeType stableEnvelope (.letE `closedStage (mkConst `Unit) closeStage (.letE `exceptionalEnvelope exceptionalEnvelopeType exceptionalEnvelope (mkConst `Collatz.synchronizedDescentProfile) true) true) true) true liftCoreM <| addDecl <| .thmDecl { name := limitingName levelParams := [] type := limitingType value := limitingValue } syntax "derive_limiting_profile " ident : command elab_rules : command | `(derive_limiting_profile $profileName:ident) => deriveLimit profileName.getId end Collatz.ProfileConstruction namespace Collatz derive_limiting_profile limitingDescentProfile /-- The limiting profile determines an exceptional positive orbit. -/ theorem limitingProfile_is_exceptional : ∃ n, Diverges n := exceptionalProfile_iff.mp limitingDescentProfile end Collatz 9:34 AM · Jul 29, 2026 · 1,777 Views ```

davidad 🌟✓ @davidad · 13h me@2024: Powerful AIs might all be misaligned; let's help humanity coordinate on formal verification and strict boxing me@2026: Too late! Powerful AIs are ~here, and some are open-weights. But some are aligned! Let's help *them* cooperate on formal verification and cybersecurity [Embedded chart: "Frontier AI's software R&D capabilities (Human-expert attention-span equivalent)" — a log-scale y-axis from 2s to 10h, x-axis quarterly from 2019 to 2028. Data points (x marks) trend upward from ~3s in 2019 to ~5h at a highlighted purple X around Q1 2026, with green/blue shaded uncertainty bands extending the trend to ~10-20h+ by 2027-2028. This appears to be a METR-style "time horizon" capability trend chart.] [Quoted tweet:] ARIA ✓ @ARIA_research · 15h In Safeguarded AI, we're funding teams to develop systems that harden our critical infrastructure from growing vulnerabilities. Programme Director @davidad warns that rapi... [cut off]