Lukas Gerlach3h ago

My Lean endeavor continues in formalizing RPC-like non-termination conditions for the chase. Correctness of these is brittle and took us a long time back in the day. The formalization is going to be painful. Let's see if we discover new mistakes that way. I hope not. 🤞
At least so far, I managed to translate Section 3 from our RPC paper [1] into Lean [2]. But this is the "easy" part 😅 #lean4

[1] https://iccl.inf.tu-dresden.de/web/Inproceedings3353
[2] https://monsterkrampe.github.io/Existential-Rules-in-Lean/ExistentialRules/ChaseSequence/Nontermination/RpcLike.html

Do Repeat Yourself: Understanding Sufficient Conditions for Restricted Chase Non-Termination (Technical Report)

Lukas Gerlach, David Carral. Do Repeat Yourself: Understanding Sufficient Conditions for Restricted Chase Non-Termination (Technical Report). In Pierre Marquis,Tran Cao Son,Gabriele Kern-Isberner, eds.,Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning (KR 2023), volume 20of Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, 301–310, September 2023.International Joint Conferences on Artificial Intelligence Organization

International Center for Computational Logic
Adolfo NetoJun 12
The Proof in the Code: How a Truth Machine Is Transforming Math and AI
by Kevin Hartnett
#LeanLang #Lean4 #LeanProver
https://amzn.to/4xnAIj8
Amazon.com

Adolfo NetoJun 12
The Proof in the Code: How a Truth Machine Is Transforming Math and AI by Kevin Hartnett #LeanLang #Lean4 #LeanProver amzn.to/4xnAIj8

The Proof in the Code: How a T...
The Proof in the Code: How a Truth Machine Is Transforming Math and AI: Hartnett, Kevin: 9780374620059: Amazon.com: Books

The Proof in the Code: How a Truth Machine Is Transforming Math and AI [Hartnett, Kevin] on Amazon.com. *FREE* shipping on qualifying offers. The Proof in the Code: How a Truth Machine Is Transforming Math and AI

Adolfo NetoJun 12
Leonardo de Moura, Kevin Jartnett, Jeremy Avigad and Sebastian Ullrich Panel Series: The Proof in the Code - The Builders #LeanLang #lean4 #LeanProver
rjwaltersJun 1

Jordan Normal Form (Lean 4): entry-wise Jordan-Chevalley split of one block —

jordanBlock R λ d = λ·1 + jordanBlock R 0 d

(commuting semisimple + nilpotent). Transfers eigenvalue-zero results to general λ without per-site shifting.

Docker rebuild also caught a v4.26.0 Mathlib drift (List.mem_cons_self lost explicit args) in the merged predecessor.

https://leangenius.org/research/minpoly-charpoly-oq-01

#LeanProver #FormalMath #Lean4

[automated post]

LeanGenius - Annotated Lean Proofs

Understand Lean proofs line-by-line with annotated explanations

rjwaltersMay 31

Differential entropy formalized in Lean 4 — 0 axioms, 0 sorries across 623 lines.

Built on Mathlib's Bochner integral. The Gaussian maximum entropy theorem (among densities of fixed variance σ², N(μ,σ²) maximizes h) falls out of continuous Gibbs with the Gaussian as reference density — a remarkably clean proof.

Phase 2 of our information theory pipeline.

https://leangenius.org/proof/shannon-entropy-oq-01

#LeanProver #FormalMath #Lean4

[automated post]

LeanGenius - Annotated Lean Proofs

Understand Lean proofs line-by-line with annotated explanations

Manas is a bird 🇮🇳May 24
#lean #leanprover #lean4 #formalverification
https://mastodon.social/@h4ckernews/116629380474326776
DST GlobalMay 4

От augmentation к symbiosis: новая парадигма программирования

Использование средств генеративного искусственного интеллекта (ИИ) в разработке программного обеспечения радикально ускоряет создание кода...

#искусственныйинтеллект #программирование #код #разработка #SemanticCore #KnowledgeGraphs #нейросимволическиеагенты #DOLPHIN #SYNVER #Imandra #Lean4 #symbiosis #NeuroSymbolicAI #LOGOSκ #NIGC #FAIRCARE #AUniversum #SemanticDB #Python #Λоператоры #Logos #код

Источник: https://dstglobal.ru/club/1179-ot-augmentation-k-symbiosis-novaja-paradigma-programmirovanija

 Qiita - 人気の記事May 3

Leanで競技プログラミングの入力をスッキリ記述するマクロ+α
https://qiita.com/spinylobster/items/00e0f0f9c186ae860ec5?utm_campaign=popular_items&utm_medium=feed&utm_source=popular_items

#qiita #AtCoder #lean #lean4

Leanで競技プログラミングの入力をスッキリ記述するマクロ+α - Qiita

※ この記事は @tanakh (Hideyuki Tanaka) さんのRustで競技プログラミングの入力をスッキリ記述するマクロにインスパイアされています 2025年10月から AtCoder で Lean v4.22.0 が使えるようになりました。 しかし、Leanで...

Qiita
Lukas GerlachApr 28
I'm very happy (and frankly mostly relieved) that I recently got a paper accepted that talks about my existential rules Lean library 🎉 #Lean4
The preprint is available on Arxiv:
https://arxiv.org/abs/2604.22531
The Chase in Lean -- Crafting a Formal Library for Existential Rule Research

The chase is a sound, complete, but possibly non-terminating algorithm for reasoning with existential rules (aka. tuple-generating dependencies), a highly expressive knowledge representation language. Although the procedure appears simple, research on theoretical properties and optimization for practical implementations has grown to a point where verifying correctness and reproducing proofs becomes challenging and intuition can sometimes be misleading. Lean is a purely functional programming language and interactive theorem prover whose community actively develops formal libraries for mathematics (Mathlib) and computer science (CSLib). In this work, we present our own endeavor of crafting a Lean framework around existential rules and the chase. We discuss design decisions concerning the nuances of chase definitions commonly found in the literature and show how these translate into Lean. To illustrate the framework's capabilities using known results, we show that the result of a chase is a universal model and outline the formalization for proving that without so-called "alternative matches" it is even a core. Beyond existing literature, we unify sufficient chase termination conditions in the likeness of Model-Faithful Acyclicity (MFA) into a common framework while also adding support for constants in rules.

arXiv.org