Lu Maltsis
@lmaltsis.bsky.social
Formal Methods, Proof Assistants, Software Security
they/them
they/them
Reposted by Lu Maltsis
@davidbessis.bsky.social The curious case of broken theorems (Mathematics shouldn't survive logical errors—yet it does). ~ David Bessis. davidbessis.substack.com/p/the-curiou... #Math #ITP #LeanProver
The curious case of broken theorems
Mathematics shouldn't survive logical errors—yet it does
davidbessis.substack.com
November 28, 2025 at 4:06 PM
@davidbessis.bsky.social The curious case of broken theorems (Mathematics shouldn't survive logical errors—yet it does). ~ David Bessis. davidbessis.substack.com/p/the-curiou... #Math #ITP #LeanProver
Reposted by Lu Maltsis
ProofGym: Unifying LLM-based theorem proving across formal systems. ~ Xinrui Li et als. openreview.net/forum?id=RrS... #ITP #LeanProver #IsabelleHOL #CoqProver #LLMs
ProofGym: Unifying LLM-Based Theorem Proving Across Formal Systems
Large language models (LLMs) have accelerated progress in automated theorem proving, but most systems remain confined to a single proof assistant, hindering cross-system reuse of reasoning patterns...
openreview.net
November 29, 2025 at 11:21 AM
ProofGym: Unifying LLM-based theorem proving across formal systems. ~ Xinrui Li et als. openreview.net/forum?id=RrS... #ITP #LeanProver #IsabelleHOL #CoqProver #LLMs
Reposted by Lu Maltsis
It’s the specification, stupid! (Seeking a significant shift in the traditional software development and verification paradigm). ~ Manfred Broy, Harald Ruess, Natarajan Shankar. dl.acm.org/doi/full/10.... #FormalVerification
November 7, 2025 at 8:09 AM
It’s the specification, stupid! (Seeking a significant shift in the traditional software development and verification paradigm). ~ Manfred Broy, Harald Ruess, Natarajan Shankar. dl.acm.org/doi/full/10.... #FormalVerification
Reposted by Lu Maltsis
Deriving an Erlang interpreter from a mechanised formal semantics of core Erlang. ~ Gergő Lajos Turán, Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, Simon Thompson. dl.acm.org/doi/abs/10.1... #ITP #Agda #FunctionalProgramming #Erlang
Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang | Proceedings of the 24th ACM SIGPLAN International Workshop on Erlang
dl.acm.org
October 13, 2025 at 11:07 AM
Deriving an Erlang interpreter from a mechanised formal semantics of core Erlang. ~ Gergő Lajos Turán, Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, Simon Thompson. dl.acm.org/doi/abs/10.1... #ITP #Agda #FunctionalProgramming #Erlang
Reposted by Lu Maltsis
Claude can (sometimes) prove it. ~ Mike Dodds. www.galois.com/articles/cla... #ITP #LeanProver #Math #AI #LLMs #Claude
September 17, 2025 at 6:33 PM
Claude can (sometimes) prove it. ~ Mike Dodds. www.galois.com/articles/cla... #ITP #LeanProver #Math #AI #LLMs #Claude
"A Conjecture Regarding SMT Instability"
ceur-ws.org/Vol-4008/SMT...
Very interesting read, also a nice summary of the workings of Z3 for someone who has only recently read "Programming Z3".
via: mastodon.social/@regehr/1150...
ceur-ws.org/Vol-4008/SMT...
Very interesting read, also a nice summary of the workings of Z3 for someone who has only recently read "Programming Z3".
via: mastodon.social/@regehr/1150...
ceur-ws.org
August 14, 2025 at 8:52 PM
"A Conjecture Regarding SMT Instability"
ceur-ws.org/Vol-4008/SMT...
Very interesting read, also a nice summary of the workings of Z3 for someone who has only recently read "Programming Z3".
via: mastodon.social/@regehr/1150...
ceur-ws.org/Vol-4008/SMT...
Very interesting read, also a nice summary of the workings of Z3 for someone who has only recently read "Programming Z3".
via: mastodon.social/@regehr/1150...
Reposted by Lu Maltsis
August 14, 2025 at 11:28 AM
Reposted by Lu Maltsis
Gödel's incompleteness theorem. ~ Thorsten Altenkirch. youtu.be/IuX8QMgy4qE #ITP #LeanProver #Logic #Math
Gödel's Incompleteness Theorem - Computerphile
YouTube video by Computerphile
youtu.be
August 8, 2025 at 7:00 AM
Gödel's incompleteness theorem. ~ Thorsten Altenkirch. youtu.be/IuX8QMgy4qE #ITP #LeanProver #Logic #Math
Recommendation:
The section "Advice to a Young Mathematician" in The Princeton Companion to Mathematics.
It's an enjoyable read. Maybe I'll get around to reading the entire book at some point.
The section "Advice to a Young Mathematician" in The Princeton Companion to Mathematics.
It's an enjoyable read. Maybe I'll get around to reading the entire book at some point.
assets.press.princeton.edu
July 23, 2025 at 4:50 PM
Recommendation:
The section "Advice to a Young Mathematician" in The Princeton Companion to Mathematics.
It's an enjoyable read. Maybe I'll get around to reading the entire book at some point.
The section "Advice to a Young Mathematician" in The Princeton Companion to Mathematics.
It's an enjoyable read. Maybe I'll get around to reading the entire book at some point.
Reposted by Lu Maltsis
This is an... unexpected use of the #LeanLang InfoView: unnamed.website/posts/bad-ap...
But we love the creativity!
#LeanProver #DevTools #Metaprogramming
But we love the creativity!
#LeanProver #DevTools #Metaprogramming
“Bad Apple!!” But It’s 3288 Lean Tactics Spamming VSCode
Writing the most useless Lean tactic ever
unnamed.website
July 8, 2025 at 8:47 PM
This is an... unexpected use of the #LeanLang InfoView: unnamed.website/posts/bad-ap...
But we love the creativity!
#LeanProver #DevTools #Metaprogramming
But we love the creativity!
#LeanProver #DevTools #Metaprogramming
via @regehr@mastodon.social (fediverse)
Very interesting article about talking to private clients about Formal Methods
www.galois.com/articles/wha...
Very interesting article about talking to private clients about Formal Methods
www.galois.com/articles/wha...
What Works (and Doesn't) Selling Formal Methods
www.galois.com
July 1, 2025 at 7:35 PM
via @regehr@mastodon.social (fediverse)
Very interesting article about talking to private clients about Formal Methods
www.galois.com/articles/wha...
Very interesting article about talking to private clients about Formal Methods
www.galois.com/articles/wha...