What is Hackers' Pub?

When Agda met Vampire

Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in implementation. We aim to improve the situation by integrating proof assistants with automated theorem provers (ATPs) in a simple way, while preserving the correctness guarantees of the former. A central difficulty arises from the fact that most ATPs operate in classical first-order logic, whereas these proof assistants are grounded in constructive dependent type theory. We identify an expressive fragment of both languages -- essentially equational Horn -- that admits sound, straightforward translations in both directions. The approach produces a prototype system for Agda forwarding proof obligations to the ATP Vampire, then transforming the resulting classical proof into a constructive proof term that Agda can type-check. The prototype automatically derives proofs concerning the properties of a complex field equipped with roots of unity, which took professional Agda developers two full days to complete. The required engineering effort is modest, and we anticipate that the methodology will extend readily to other ATPs and proof assistants.

arxiv.org · arXiv.org

List - Mastodon documentation

Represents a list of some users that the authenticated user follows.

docs.joinmastodon.org

Formalized Run-Time Analysis of Active Learning -- Coalgebraically in Agda

The objective of automata learning is to reconstruct the implementation of a hidden automaton, to which only a teacher has access. The learner can ask certain kinds of queries to the teacher to gain more knowledge about the hidden automaton. The run-time of such a learning algorithm is then measured in the number of queries it takes until the hidden automaton is successfully reconstructed, which is usually parametric in the number of states of that hidden automaton. How can we prove such a run-time complexity of learning algorithms in a proof assistant if we do not have the hidden automaton and the number of states available? In the present paper, we solve this by considering learning algorithms themselves as generalized automata, more specifically as coalgebras. We introduce formal and yet compact definitions of what a learner and a teacher is, which make it easy to prove upper and lower bounds of different kinds of learning games in the proof assistant Agda. As a running example, we discuss the common number guessing game where a teacher thinks of a natural number and answers guesses by the learner with `correct', `too high', or `too low'. To demonstrate our framework, we formally prove in Agda that both the lower and upper bound on number of guesses by the learner is $\mathcal{O}(\log n)$, where $n$ is the teacher's secret number.

arxiv.org · arXiv.org

MastoBlaster — A snac-first Fediverse client

MastoBlaster is a lightweight, privacy-first Fediverse client with first-class snac support, EXIF stripping, Markdown posting, and on-device alt text generation.

mastoblaster.app

Classifying 2-Groups in Homotopy Type Theory

- Theory of computation -> Type theory.Constructive mathematics.Logic and verification.- Mathematics of computing -> Algebraic topology.

phart3.github.io

Verifying the Hashgraph Consensus Algorithm

The Hashgraph consensus algorithm is an algorithm for asynchronous Byzantine fault tolerance intended for distributed shared ledgers. Its main distinguishing characteristic is it achieves consensus without exchanging any extra messages; each participant's votes can be determined from public information, so votes need not be transmitted. In this paper, we discuss our experience formalizing the Hashgraph algorithm and its correctness proof using the Coq proof assistant. The paper is self-contained; it includes a complete discussion of the algorithm and its correctness argument in English.

arxiv.org · arXiv.org

Stripe publishes 2025 annual letter and announces tender offer to provide liquidity to current and former employees

Stripe announces tender offer to provide liquidity to current and former employees; publishes 2025 annual letter

stripe.com

A Formal Correctness Proof of Edmonds’ Blossom Shrinking Algorithm

Mohammad Abdulaziz · Journal of Automated Reasoning, https://doi.org/10.1007/s10817-026-09747-y

link.springer.com

Lean Formalization of Generalization Error Bound by Rademacher Complexity

We formalize the generalization error bound using Rademacher complexity in the Lean 4 theorem prover. Generalization error quantifies the gap between a learning machine's performance on given training data versus unseen test data, and Rademacher complexity serves as an estimate of this error based on the complexity of learning machines, or hypothesis class. Unlike traditional methods such as PAC learning and VC dimension, Rademacher complexity is applicable across diverse machine learning scenarios including deep learning and kernel methods. We formalize key concepts and theorems, including the empirical and population Rademacher complexities, and establish generalization error bounds through formal proofs of McDiarmid's inequality, Hoeffding's lemma, and symmetrization arguments.

arxiv.org · arXiv.org

Ricardo Mendes

24 February 2026 Fedi Fedify Indiekit ActivityPub The first time you click a Fediverse button on my site, you’ll be asked to enter your home instance — in other words, your own Fediverse server. This...

rmendes.net · Ricardo Mendes

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4

In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a conjecture in a proof assistant. In this work, we introduce several novel concepts and capabilities to address obstacles faced by machine-assisted theorem proving. We first present a set of \textbf{atomic tactics}, a small finite set of tactics capable of proving any provable statement in Lean. We then introduce a \textbf{transposing atomization} algorithm which turns arbitrary proof expressions into a series of atomic tactics. We next introduce the \textbf{ExprGraph} data structure, which provides a succinct representation for Lean expressions. Finally, we present the \textbf{Nazrin Prover}, a graph neural network-based theorem proving agent using atomic tactics and ExprGraph. Nazrin circumvents many challenges faced by existing proving agents by exclusively dispatching atomic tactics, and it is robust enough to both train and evaluate on consumer-grade hardware. We demonstrate the potential of tools like Nazrin using theorems from Lean's standard library and from Mathlib.

arxiv.org · arXiv.org

Formalization of Two Fixed-Point Algorithms in Hilbert Spaces

Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel'ski\uı--Mann iteration and Halpern iteration are two widely used schemes. In this work, we formalize the convergence of these two fixed-point algorithms in the interactive theorem prover Lean4 based on type dependent theory. To this end, weak convergence and topological properties in the infinite-dimensional real Hilbert space are formalized. Definition and properties of nonexpansive operators are also provided. As a useful tool in convex analysis, we then formalize the Fejér monotone sequence. Building on these foundations, we verify the convergence of both the iteration schemes. Our formalization provides reusable components for machine-checked convergence analysis of fixed-point iterations and theories of convex analysis in real Hilbert spaces. Our code is available at https://github.com/TTony2019/fixed-point-iterations-in-lean.

arxiv.org · arXiv.org

Integral Curves and Flows on Banach Manifolds in Lean

We present a formalisation of the existence and uniqueness theorems of integral curves of vector fields on Banach manifolds in the Lean theorem prover. First, we formalize properties of differential equations on Banach spaces (the Picard-Lindelöf theorem, the Grönwall inequality, and corollaries), and then transfer results to abstract Banach manifolds. Built upon the differential and integral calculus and Banach manifolds libraries in Mathlib, our work aims to lay the foundation for dynamical systems and differential geometry libraries that are general, robust, and friendly to classical mathematicians.

arxiv.org · arXiv.org

Formalizing Gröbner Basis Theory in Lean

We present a formalization of Gröbner basis theory in Lean 4, built on top of Mathlib's infrastructure for multivariate polynomials and monomial orders. Our development covers the core foundations of Gröbner basis theory, including polynomial division with remainder, Buchberger's criterion, and the existence and uniqueness of reduced Gröbner bases. We develop the theory uniformly for polynomial rings indexed by arbitrary types, enabling the treatment of Gröbner bases in rings with infinitely many variables. Furthermore, we connect the finite and infinite settings by showing that infinite-variable reduced Gröbner bases can be characterized via reduced Gröbner bases on finite-variable subrings through monomial-order embeddings and filter-based limit constructions.

arxiv.org · arXiv.org

We installed a single turnstile to feel secure

After the acquisition by a much larger company, security became a top priority. Our company occupied three tall buildings, each at least 13 stories high. Key card readers were installed next to every

idiallo.com · Ibrahim Diallo Blog

Datenschutz-Reform: Mitgliedstaaten gehen auf Abstand zu Plänen der EU-Kommission

Es ist das erste Signal des Rates im Ringen um den sogenannten Datenomnibus: In einem ersten Positionierungsentwurf stellen sich die Mitgliedstaaten gegen mehrere Vorschläge der EU-Kommission, die von Datenschutz-Expert:innen kritisiert worden waren. Wir veröffentlichen den Zwischenstand.

netzpolitik.org · netzpolitik.org

Mastodon 4.5.7 by mistydemeo · Pull Request #1389 · hometown-fork/hometown

It figures a new release would come out immediately after we release 1.2.0 😅 This is a minor bugfix release though, and was very easy to cherry-pick in. https://github.com/mastodon/mastodon/release...

github.com · GitHub

L'italiano secondo il metodo natura || Capitolo 1: La famiglia Rossi

Il metodo natura per imparare l'italiano. In questa serie leggiamo insieme "L'italiano secondo il metodo natura" (Italian by the Natura Method) di Arthur Jen...

www.youtube.com · YouTube

A Potentially Infinite Number of AI Homer Simpson ‘Cover Songs’ Have ‘Poisoned’ Soulseek

A troll is sharing more than 2,000 Homer songs masquerading as originals—and there may be plenty more on their way.

www.vice.com · VICE

MastoBlaster — A snac-first Fediverse client

MastoBlaster is a lightweight, privacy-first Fediverse client with first-class snac support, EXIF stripping, Markdown posting, and on-device alt text generation.

mastoblaster.app

A Weapon to Destroy a God

A Machine Built to End War, is always a Machine Built to Continue War. | Watch my exclusive video 'When a Weapon Dreams of Peace' by joining Nebula at https:...

www.youtube.com · YouTube