What is Hackers' Pub?

minimitra

minimitra

codeberg.org · Codeberg.org

Osaka: Kansai Airport Proud to Have Never Lost Single Piece of Luggage;‘World’s Best Airport for Baggage Delivery’

<p>IZUMI-SANO, Osaka — Kansai Airport is proud to have never had a lost baggage incident in the 30 years since it opened in 1994, earning recognition as the airport with the world’s best baggage service.</p>

japannews.yomiuri.co.jp

I Taught My Dog to Vibe Code Games | Caleb Leak

My cavapoo Momo vibe coded playable Godot games. All I had to do was teach her to type, route her input to Claude Code, and build the right tools.

www.calebleak.com

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs

Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and such DSLs is a tedious engineering chore. To simplify this task, we present DSLean, a framework for bidirectional translation between expressions in the Lean proof assistant and external syntax. DSLean requires only a specification of an external language and its Lean equivalents, abstracting away meta-level implementation details. We demonstrate DSLean's capabilities by implementing three new automation tactics, providing access to external solvers for interval arithmetic, ordinary differential equations, and ring ideal membership.

arxiv.org · arXiv.org

Tiny Tapeout Submission Form: for shuttles & workshops

swisschips.ethz.ch · SwissChips

AIのテストコードは信用するな🙅‍♂️

zenn.dev · Zenn

Samsung's Galaxy Upcycle promised to make old phones useful, then won an award for giving up

Your old phone could have been so much more.

www.xda-developers.com · XDA

fedicat/Sources/Fedicat/Platforms/MastoAPI/Snac.swift at main

fedicat - issues and non-UI code for the Fedicat fediverse client

codeberg.org · Codeberg.org

Large Language Model Reasoning Failures

Large Language Models (LLMs) have exhibited remarkable reasoning capabilities, achieving impressive results across a wide range of tasks. Despite these advances, significant reasoning failures persist, occurring even in seemingly simple scenarios. To systematically understand and address these shortcomings, we present the first comprehensive survey dedicated to reasoning failures in LLMs. We introduce a novel categorization framework that distinguishes reasoning into embodied and non-embodied types, with the latter further subdivided into informal (intuitive) and formal (logical) reasoning. In parallel, we classify reasoning failures along a complementary axis into three types: fundamental failures intrinsic to LLM architectures that broadly affect downstream tasks; application-specific limitations that manifest in particular domains; and robustness issues characterized by inconsistent performance across minor variations. For each reasoning failure, we provide a clear definition, analyze existing studies, explore root causes, and present mitigation strategies. By unifying fragmented research efforts, our survey provides a structured perspective on systemic weaknesses in LLM reasoning, offering valuable insights and guiding future research towards building stronger, more reliable, and robust reasoning capabilities. We additionally release a comprehensive collection of research works on LLM reasoning failures, as a GitHub repository at https://github.com/Peiyang-Song/Awesome-LLM-Reasoning-Failures, to provide an easy entry point to this area.

arxiv.org · arXiv.org

M2F: Automated Formalization of Mathematical Literature at Scale

Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as it requires managing cross-file dependencies, resolving imports, and ensuring that entire projects compile end-to-end. We present M2F (Math-to-Formal), the first agentic framework for end-to-end, project-scale autoformalization in Lean. The framework operates in two stages. The statement compilation stage splits the document into atomic blocks, orders them via inferred dependencies, and repairs declaration skeletons until the project compiles, allowing placeholders in proofs. The proof repair stage closes these holes under fixed signatures using goal-conditioned local edits. Throughout both stages, M2F keeps the verifier in the loop, committing edits only when toolchain feedback confirms improvement. In approximately three weeks, M2F converts long-form mathematical sources into a project-scale Lean library of 153,853 lines from 479 pages textbooks on real analysis and convex analysis, fully formalized as Lean declarations with accompanying proofs. This represents textbook-scale formalization at a pace that would typically require months or years of expert effort. On FATE-H, we achieve $96\%$ proof success (vs.\ $80\%$ for a strong baseline). Together, these results demonstrate that practical, large-scale automated formalization of mathematical literature is within reach. The full generated Lean code from our runs is available at https://github.com/optsuite/ReasBook.git.

arxiv.org · arXiv.org

Haskell meets Evariste

Since its birth as a new scientific body of knowledge in the late 1950s, computer programming has become a fundamental skill needed in many other disciplines. However, programming is not easy, it is prone to errors and code re-use is key for productivity. This calls for high-quality documentation in software libraries, which is quite often not the case. Taking a few Haskell functions available from the Hackage repository as case-studies, and comparing their descriptions with similar functions in other languages, this paper shows how clarity and good conceptual design can be achieved by following a so-called easy-hard-split formal strategy that is quite general and productive, even if used informally. This strategy is easy to use in functional programming and can be applied to both program analysis and synthesis.

arxiv.org · arXiv.org

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