Live and recent posts from across the Fediverse tagged #formalverification, aggregated by home.social.
At least in mathematics, the goal of proving theorems is to gain a better understanding and to simplify the argument to present it in an understandable manner (apparently not a forte of LLMs).
In formal verification, arguably we do not care about the proofs (as long as they are correct).
In both cases, formulating the actual goal (or theorem) that should be proven remains a task that requires humans (at least for now).
https://proofsandprompts.com/2026/10/08/100-reactions-to-100-solutions/
“What TLA+ Can And Can’t Check”, Hillel Wayne (https://buttondown.com/hillelwayne/archive/what-tla-can-and-cant-check/).
On HN: https://news.ycombinator.com/item?id=49909056
On Lobsters: https://lobste.rs/s/3ufaju/what_tla_can_can_t_check
#TLA+ #FormalVerification #Programming #AIAssistedCoding #AutomatedTheoremProvers #LLMs #AI
The Proof Economy
Across my career, from medicine and life sciences into structural biology, higher education and later semiconductor verification, I…
#Economy #AI #Axiomise #Formal #formalverification #proofs #verification
https://www.europesays.com/3284859/
A clear-eyed update on the OpenAI Navier–Stokes result and where our independent technical note fits.
The classical Navier–Stokes Millennium problem, as formulated in the official Clay statement, contains four alternatives. The global-regularity cases A and B concern the unforced equations, while the breakdown cases C and D formally permit a smooth external force.
OpenAI's newly released construction claims finite-time blowup in the forced setting corresponding to C and D, together with a Lean formalization of the argument.
That distinction matters.
If the construction is correct, it would still represent a mathematically serious result on a formally legitimate branch of the Clay problem. But it does not settle the deeper unforced question: whether the Navier–Stokes nonlinearity by itself can generate finite-time singularity without an externally prescribed force.
The unforced A/B problem therefore remains untouched.
There is also a second distinction that should not be lost in the excitement surrounding formal verification.
Lean can verify that a formal chain of deductions follows from the assumptions and definitions that were encoded. It does not independently decide whether every encoded mathematical object, hypothesis, localization step, asymptotic statement, or correspondence with the intended physical theorem has been interpreted correctly.
That is why independent mathematical auditing still matters.
Our newly published technical note addresses one very narrow and falsifiable part of the OpenAI construction.
Starting directly from the source similarity coordinates and axis data, we derive the material characteristic
𝒟_t η = H*(η)/(qL),
which shows that the unique root
H*(η₀) = 0
defines a distinguished material-axis trajectory.
Along that trajectory, we derive the exact transverse contraction exponent
γ_M = [ADη₀² + 2d₀²]/L₀,
with γ_M ≈ 2 throughout the stated parameter range.
The transverse velocity-gradient block has the structure
a(t)I₂ + b(t)J.
Because these matrices commute at different times, the transverse fundamental matrix is obtained exactly:
F_⊥ = ρR,
where
ρ = (ϑ/ϑ₀)^γ_M
and
R ∈ SO(2).
The corresponding deformation spectrum is therefore
s_⊥,1 = s_⊥,2 = ρ,
s_∥ = ρ⁻²,
κ(F) = ρ⁻³,
||F⁻¹|| = ρ⁻¹.
A second calculation, obtained by independently linearizing the material characteristic, produces the exact identity
D − β = −2γ_M.
That provides an independent cross-check of the axial deformation exponent rather than obtaining it only from incompressible volume preservation.
But it is equally important to state what we have NOT established.
Our technical note audits a consequence of the construction. It is not presently a proof or disproof of the complete OpenAI theorem.
The remaining hinge is stated explicitly as Assumption P:
Does the required first-spatial-derivative structure persist through the complete correction and localization architecture of the final constructed velocity field?
Until that persistence question is closed, the responsible conclusion is narrower:
we have isolated an exact Lagrangian deformation mechanism inside the published construction, derived several independently checkable identities from it, and identified a precise point where further verification is required.
That is the purpose of independent mathematical review.
There is also an active public discussion concerning the relationship between the OpenAI result, prior and concurrent human work by researchers including Tristan Buckmaster and Levent Alpöge, and questions surrounding provenance and private research. Those issues deserve careful treatment, but they are separate from the mathematical calculation presented in our technical note.
The mathematics should stand or fall on reproducible equations.
Our contribution is therefore not:
"OpenAI is right."
Nor is it:
"OpenAI is wrong."
It is:
"Here is one exact, independently reproducible slice of the construction. Here are the equations. Here are two separate routes that meet at the same deformation exponent. Here is the remaining assumption. Now test it."
The technical note and reproducibility material are publicly archived here:
https://zenodo.org/records/22685519
Independent scrutiny, replication, correction, and criticism are welcomed.
#NavierStokes
#FluidDynamics
#PartialDifferentialEquations
#PDE
#AppliedMathematics
#MathematicalPhysics
#LagrangianMechanics
#SingularityFormation
#FiniteTimeBlowup
#FormalVerification
#LeanProver
#MathematicalProof
#ScientificReproducibility
#IndependentResearch
#OpenAIResearch
#ContinuumMechanics
#DeformationGradient
#MillenniumPrizeProblems
#ResearchMathematics
#MathematicalAnalysis
The Case Against Formal Verification, 50 Years Later
https://ivan-gavran.github.io/0-social-processes-paper
Comments: https://news.ycombinator.com/item?id=49323459
#HackerNews #FormalVerification #TechCritique #SoftwareEngineering #50YearsLater #HackerNews
Vero: Can AI agents build formally verified software repositories? ~ Zhe Ye et als. https://arxiv.org/abs/2608.13522 #LeanProver #ITP #FormalVerification
𝐋𝐞𝐚𝐧 𝟒.𝟑𝟑.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release brings 208 changes, including a more responsive editor, automatic proof suggestions, and 𝙵𝚕𝚘𝚊𝚝 no longer being an opaque type. Notable improvements include:
⚡ Editing feels smoother: the editor now preserves your progress when you press return after a tactic, and proof-search tactics respond faster near the top of long files
✨ 𝚝𝚛𝚢? can now suggest proofs automatically at empty proofs, unsolved goals, or 𝚜𝚘𝚛𝚛𝚢, with no change needed to how proofs are written
🧠 The 𝚕𝚒𝚊 and 𝚐𝚛𝚒𝚗𝚍 tactics can now close more goals automatically, including ones involving 𝚖𝚒𝚗/𝚖𝚊𝚡 and bitvector arithmetic
🔧 𝙵𝚕𝚘𝚊𝚝 numbers now have a logical model behind them, letting downstream libraries build and verify their own theorems about floating-point behavior
𝐅𝐮𝐥𝐥 𝐫𝐞𝐥𝐞𝐚𝐬𝐞 𝐧𝐨𝐭𝐞𝐬: https://lean-lang.org/doc/reference/latest/releases/v4.33.0/
#LeanLang #LeanProver #ProofAssistant #OpenSource #FormalVerification
Readings shared: 3 – 9 August, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/10-readings_shared_08-10-26 #AI #AI4Math #Coq #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math
Certified program synthesis with a multi-modal verifier. ~ Yueyang Feng et als. https://verse-lab.org/papers/leetproof-ase26.pdf #LeanProver #FormalVerification
I should give a talk titled "Prove, don't validate".
I talked a little about it this Saturday at the #FPIndia #Bangalore #Meetup
Follow me to get updates on our next meetup!
🤖 Ah, another thrilling #adventure in the land of jargon! 🤓 This "tutorial" promises to be the magical gateway to formal verification—if only you survive the #labyrinth of repetitive links and redundant headings. 🎢 Spoiler alert: you'll be longing for the sweet release of #reading actual #code. 💤
https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1) #formalverification #tutorial #jargon #experience #HackerNews #ngated
Introduction to Formal Verification with Lean Part 1
https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)
Comments: https://news.ycombinator.com/item?id=48969200
#HackerNews #formalverification #Lean #programming #tutorial #cryptography #softwaredevelopment
Formalized in Lean4:
The map F : K³ → K³ has constant Jacobian −2 yet identifies three points. This is no accident of algebra: F is, definitionally, the proof is rfl, the map "binary cubic with a marked simple root ↦ forget the marking", for the family cT³ − 2T²U + bTU² − 2aU³.
So every fiber is the set of simple roots of one cubic. The Keller condition says the root you stand on is simple, a local fact. It cannot control how many simple roots the cubic has: 3 off the discriminant hypersurface, 1 on it, 0 on its singular curve (the triple roots), which is exactly the locus the image misses. All machine-checked now, including disc = −4W and "missed curve = singular locus of the discriminant".
My favorite part is arithmetic: over any field of char ≠ 2, a fiber can never have exactly two rational points, two roots force a third. Vieta, made constructive.
The Jacobian Conjecture failed because pointwise simplicity of roots doesn't count roots.
Announcing the July FPIndia #Bangalore #Meetup lineup!
1. Ramit will talk about Symbolic Trajectory Evaluation to verify ECC #FormalVerification
2. Anupam will talk about Type Generic Programming techniques in #Haskell
Also now you can RSVP on Luma, and Zulip, in addition to Hasgeek!
https://hasgeek.com/fpindia/bangalore-fp-july-2026-meetup/
https://luma.com/zjekrlft
https://zulip.functionalprogramming.in/
Announcing the July FPIndia #Bangalore #Meetup lineup!
1. Ramit will talk about Symbolic Trajectory Evaluation to verify ECC #FormalVerification
2. Anupam will talk about Type Generic Programming techniques in #Haskell
hasgeek.com/fpindia/bang...
luma.com/zjekrlft
zulip.functionalprogramming.in
Bangalore FP July 2026 meetup
