#proofassistant — Public Fediverse posts

𝐋𝐞𝐚𝐧 𝟒.𝟑𝟑.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! 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

𝐋𝐞𝐚𝐧 𝟒.𝟑𝟑.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! 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

A computer found one solution to a hard model-building problem. Then we proved you will *always* find one — and machine-checked the proof in Lean 4. 🧮

The setting: which fermions complete a quark block in a 6D \(SU(4)\) gauge–Higgs model on an orbifold, so that every local consistency condition (anomalies + "tadpoles") cancels? These are exact integer / representation-theory conditions over \(SU(4)\) weights.

One witness is easy to distrust — a fluke? The structural answer is no. Writing the anomaly map \(A\) and the tadpole map \(\Theta\) as linear functionals of the added matter, two exact facts settle it:
• \(\operatorname{rank}[A;\Theta]=8+2=10\): the tadpole is *independent* of the anomalies — no conserved invariant traps it;
• anomaly-neutral additions realise *every* tadpole direction (Farkas certificates), so their cone is all of \(\mathbb{R}^2\).

Hence *every* anomaly-free completion is tadpole-compatible: an Existence theorem, not luck. The certificate is checked by the Lean 4 kernel, depending only on propext. The same rank+cone test ships as a reusable tool for any orbifold model. Honest scope: one infrared step stays open.

📄 https://zenodo.org/records/21432626
💻 https://github.com/karlesmarin/ghu-su4-completion

#Lean4 #FormalMath #ProofAssistant #RepresentationTheory #Maths #Physics

A computer found one solution to a hard model-building problem. Then we proved you will *always* find one — and machine-checked the proof in Lean 4. 🧮

The setting: which fermions complete a quark block in a 6D \(SU(4)\) gauge–Higgs model on an orbifold, so that every local consistency condition (anomalies + "tadpoles") cancels? These are exact integer / representation-theory conditions over \(SU(4)\) weights.

One witness is easy to distrust — a fluke? The structural answer is no. Writing the anomaly map \(A\) and the tadpole map \(\Theta\) as linear functionals of the added matter, two exact facts settle it:
• \(\operatorname{rank}[A;\Theta]=8+2=10\): the tadpole is *independent* of the anomalies — no conserved invariant traps it;
• anomaly-neutral additions realise *every* tadpole direction (Farkas certificates), so their cone is all of \(\mathbb{R}^2\).

Hence *every* anomaly-free completion is tadpole-compatible: an Existence theorem, not luck. The certificate is checked by the Lean 4 kernel, depending only on propext. The same rank+cone test ships as a reusable tool for any orbifold model. Honest scope: one infrared step stays open.

📄 https://zenodo.org/records/21432626
💻 https://github.com/karlesmarin/ghu-su4-completion

#Lean4 #FormalMath #ProofAssistant #RepresentationTheory #Maths #Physics

I’m happy to announce that the 43rd Agda Implementors’ Meeting will take place in Rzeszów, Poland from 2026-10-12 to 2026-10-17 2026-10-19 to 2026-10-24 (Mon to Sat). Everyone interested in Agda is welcome to attend, no matter whether you are a veteran or a beginner, and whether you are working on Agda or in Agda. More information about the venue and the registration will appear soon on the wiki page at https://wiki.portal.chalmers.se/agda/Main/AIMXLIII.

Edit: the dates were moved by one week, it is now 19-24 October!

#Agda #DependentTypes #ProofAssistant

I’m happy to announce that the 43rd Agda Implementors’ Meeting will take place in Rzeszów, Poland from 2026-10-12 to 2026-10-17 2026-10-19 to 2026-10-24 (Mon to Sat). Everyone interested in Agda is welcome to attend, no matter whether you are a veteran or a beginner, and whether you are working on Agda or in Agda. More information about the venue and the registration will appear soon on the wiki page at https://wiki.portal.chalmers.se/agda/Main/AIMXLIII.

Edit: the dates were moved by one week, it is now 19-24 October!

#Agda #DependentTypes #ProofAssistant

Lean 4.31.0 is released.

This consolidation-heavy release brings 305 changes. For those working on verified software: repeat/while loops are now verifiable without requiring source changes, expanding through whileM to support a one-step unfolding lemma. The new experimental mvcgen' tactic, reimplemented from the ground up on the SymM-based symbolic evaluation framework, can outperform mvcgen by a factor of over 100x on some synthetic benchmarks.

Library authors and package maintainers also gain a built-in linting framework through lake lint, with linters upstreamed from Batteries and Mathlib.

Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.31.0/

#LeanLang #LeanProver #ProofAssistant #FormalVerification

Lean 4.31.0 is released.

This consolidation-heavy release brings 305 changes. For those working on verified software: repeat/while loops are now verifiable without requiring source changes, expanding through whileM to support a one-step unfolding lemma. The new experimental mvcgen' tactic, reimplemented from the ground up on the SymM-based symbolic evaluation framework, can outperform mvcgen by a factor of over 100x on some synthetic benchmarks.

Library authors and package maintainers also gain a built-in linting framework through lake lint, with linters upstreamed from Batteries and Mathlib.

Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.31.0/

#LeanLang #LeanProver #ProofAssistant #FormalVerification

Functional Data Structures and Algorithms: a Proof Assistant Approach

https://fdsa-book.net/

#HackerNews #FunctionalDataStructures #Algorithms #ProofAssistant #Programming #HN

Functional Data Structures and Algorithms: a Proof Assistant Approach

https://fdsa-book.net/

#HackerNews #FunctionalDataStructures #Algorithms #ProofAssistant #Programming #HN

🤓 Ah yes, the riveting saga of "normal-order syntax-rules" and the elusive call/cc fix-point, where syntax rules magically transform into a proof assistant. 🧙‍♂️ Because what better way to celebrate Daniel P. Friedman than with a marathon of indecipherable jargon and fewer common examples no one asked for. 🎉
https://okmij.org/ftp/Scheme/callcc-calc-page.html #normalordersyntax #syntaxrules #callcc #proofassistant #DanielPFriedman #programmingjargon #HackerNews #ngated

🤓 Ah yes, the riveting saga of "normal-order syntax-rules" and the elusive call/cc fix-point, where syntax rules magically transform into a proof assistant. 🧙‍♂️ Because what better way to celebrate Daniel P. Friedman than with a marathon of indecipherable jargon and fewer common examples no one asked for. 🎉
https://okmij.org/ftp/Scheme/callcc-calc-page.html #normalordersyntax #syntaxrules #callcc #proofassistant #DanielPFriedman #programmingjargon #HackerNews #ngated

Readings shared August 1, 2025. https://jaalonso.github.io/vestigium/posts/2025/08/02-readings_shared_08-01-25 #Haskell #LeanProver #Math #ProofAssistant

Readings shared August 1, 2025. https://jaalonso.github.io/vestigium/posts/2025/08/02-readings_shared_08-01-25 #Haskell #LeanProver #Math #ProofAssistant

Readings shared July 31, 2025. https://jaalonso.github.io/vestigium/posts/2025/08/01-readings_shared_08-01-25 FunctionalProgramming #Haskell #LeanProver #Math #ProofAssistant

Readings shared July 31, 2025. https://jaalonso.github.io/vestigium/posts/2025/08/01-readings_shared_08-01-25 FunctionalProgramming #Haskell #LeanProver #Math #ProofAssistant

The math is haunted. ~ Dan Abramov. https://overreacted.io/the-math-is-haunted/ #ProofAssistant #LeanProver #Math

The math is haunted. ~ Dan Abramov. https://overreacted.io/the-math-is-haunted/ #ProofAssistant #LeanProver #Math

Universal pairs for diophantine equations (in Isabelle/HOL). ~ Marco David et als. https://www.isa-afp.org/entries/Diophantine_Universal_Pairs.html #ITP #ProofAssistant #IsabelleHOL #Math

Universal pairs for diophantine equations (in Isabelle/HOL). ~ Marco David et als. https://www.isa-afp.org/entries/Diophantine_Universal_Pairs.html #ITP #ProofAssistant #IsabelleHOL #Math

Readings shared July 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/30-readings_shared_07-29-25 #CoqProver #FormalVerification #FunctionalProgramming #Haskell #IMO #ITP #LLMs #LeanProver #MachineLearning #Math #ProofAssistant #Rocq #Rust

Readings shared July 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/30-readings_shared_07-29-25 #CoqProver #FormalVerification #FunctionalProgramming #Haskell #IMO #ITP #LLMs #LeanProver #MachineLearning #Math #ProofAssistant #Rocq #Rust

Harmonic's IMO 2025 results (Harmonic's model Aristotle achieved gold medal performance, solving 5 problems). https://github.com/harmonic-ai/IMO2025/ #FormalVerification #ProofAssistant #LeanProver #LLMs #Math #IMO

Harmonic's IMO 2025 results (Harmonic's model Aristotle achieved gold medal performance, solving 5 problems). https://github.com/harmonic-ai/IMO2025/ #FormalVerification #ProofAssistant #LeanProver #LLMs #Math #IMO

Readings shared July 28, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/29-readings_shared_07-28-25 #FormalVerification #FunctionalProgramming #Haskell #LeanProver #Logic #Math #ProofAssistant

Readings shared July 28, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/29-readings_shared_07-28-25 #FormalVerification #FunctionalProgramming #Haskell #LeanProver #Logic #Math #ProofAssistant

Formalized formal logic (in Lean4). https://formalizedformallogic.github.io/Book/ #FormalVerification #ProofAssistant #LeanProver #Logic #Math

Formalized formal logic (in Lean4). https://formalizedformallogic.github.io/Book/ #FormalVerification #ProofAssistant #LeanProver #Logic #Math

Gödel's first incompleteness theorem (in Lean4). https://formalizedformallogic.github.io/Book/first_order/goedel1.html #FormalVerification #ProofAssistant #LeanProver #Logic #Math

Gödel's first incompleteness theorem (in Lean4). https://formalizedformallogic.github.io/Book/first_order/goedel1.html #FormalVerification #ProofAssistant #LeanProver #Logic #Math

Encoding finite state automata in Agda using coinduction (Evaluating the support for coinduction in Agda). ~ Noky Soekarman. https://repository.tudelft.nl/file/File_56e70e9e-4f41-429c-a383-20c1bf61c16a #FormalVerification #ProofAssistant #Agda

Encoding finite state automata in Agda using coinduction (Evaluating the support for coinduction in Agda). ~ Noky Soekarman. https://repository.tudelft.nl/file/File_56e70e9e-4f41-429c-a383-20c1bf61c16a #FormalVerification #ProofAssistant #Agda

Modelling cyclic structures in Agda (Evaluating Agda’s coinduction through modelling graphs). ~ Faizel Mangroe. https://repository.tudelft.nl/file/File_6466eb89-91b7-4561-9933-236ae3f9e15b #ProofAssistant #Agda

Modelling cyclic structures in Agda (Evaluating Agda’s coinduction through modelling graphs). ~ Faizel Mangroe. https://repository.tudelft.nl/file/File_6466eb89-91b7-4561-9933-236ae3f9e15b #ProofAssistant #Agda

(and if anyone has some research grants, I'd appreciate being given some pointers to them)

#ProgrammingLanguage #ProofAssistant #mathematics

In the past couple days we successfully got our new language to host a hello world webserver and open a hello world desktop gui, and pushed past 2ksloc of some nontrivial bootstrapping, prelude, and tests being maintained. There's still a lot to do, like implement all the missing features to make non-hello-world projects, and the typechecker is held together with duct tape and bailing wire and it really shows sometimes. Volunteers welcome if you want to suffer with me on a really cool project to push the boundaries on what's possible in a practical programming language and proof assistant.

#ProgrammingLanguage #ProofAssistant #mathematics

I am listening to the @ttforall podcast with Jimmy Koppel on which parts of CS theory all software engineers should learn about (see also his blog post from 2021 on why programmers should(n't) learn theory). Now I'm curious to learn which parts of "theory" you think are the most useful for a software engineer.

Please boost this so this also finds an audience beyond the types community!

#SoftwareEngineering #Education #TypeTheory #ProgramVerification #AbstractInterpretation #ProofAssistant #HoareLogic #ModelChecking #SMT #OperationalSemantics #CategoryTheory #DomainTheory