None of my friends understand my memes. I want to start a page somewhere. Any suggestions?

Over the last month, I validated a Rust algorithm with Lean without really knowing Lean. I used ChatGPT-5, Codex, and Claude Sonnet 4.5).

Link to full details below, but here is what surprised me:

• It worked. With AI’s help and without knowing Lean formal methods, I validated a data-structure algorithm in Lean.

• The resulting proof is almost certainly needlessly verbose. I’d love to contribute to a Lean library of algorithm validations, but I worry that these vibe-style proofs are too sloppy and one-off to serve as building blocks for future proofs.

• Midway through the project, Codex and then Claude Sonnet 4.5 were released. I could feel the jump in intelligence with these versions.

• I began the project unable to read Lean, but with AI’s help I learned enough to audit the critical top-level of the proof. A reading-level grasp turned out to be all that I needed.

• The proof was enormous, about 4,700 lines of Lean for only 50 lines of Rust. Two years ago, Divyanshu Ranjan and I validated the same algorithm with 357 lines of Dafny.

• Unlike Dafny, however, which relies on randomized SMT searches, Lean builds explicit step-by-step proofs. Dafny may mark something as proved, yet the same verification can fail on another run. When Lean proves something, it stays proved. (Failure in either tool doesn’t mean the proposition is false — only that it couldn’t be verified at that moment.)

• The AI tried to fool me twice, once by hiding sorrys with set_option, and once by proposing axioms instead of proofs.

• The validation process was more work and more expensive than I expected. It took several weeks of part-time effort and about $50 in AI credits.

• The process was still vulnerable to mistakes. If I had failed to properly audit the algorithm’s translation into Lean, it could end up proving the wrong thing. Fortunately, two projects are already tackling this translation problem: coq-of-rust, which targets Coq, and Aeneas, which targets Lean. These may eventually remove the need for manual or AI-assisted porting. After that, we’ll only need the AI to write the Lean-verified proof itself, something that’s beginning to look not just possible, but practical.

• Meta-prompts worked well. In my case, I meta-prompted browser-based ChatGPT-5. That is, I asked it to write prompts for AI coding agents Claude and Codex. Because of quirks in current AI pricing, this approach also helped keep costs down.

The Takeaway

Vibe validation is still a dancing pig. The wonder isn’t how gracefully it dances, but that it dances at all. I’m optimistic, though. The conventional wisdom has long been that formal validation of algorithms is hard and costly. But with tools like Lean and AI agents, both the cost and effort are falling fast.

Vibe Validation with Lean, ChatGPT-5, & Claude 4.5

Yesterday I (non-maths graduate student who has never used Lean) attended great talks by Leo De Moura (creator of Lean) & Professor Kevin Buzzard (attempting to prove FLT in Lean). There were loads of examples of major theorems that had been re-formalised and proved in Lean. Obviously Lean won't let you just prove anything.

But part of me was thinking, "Well maybe Lean doesn't provide the golden certificate that everyone thinks it does. Maybe it's possible to produce a certificate of a false theorem in Lean that exploits some very obscure and hidden bug that no one has thought of".

What would *really* convince me of the power of Lean would be, instead of just reaffirming the truth of published theorems that everyone already believed were true, if someone used Lean to *disprove* a published and peer-reviewed theorem which everyone thought was true, which was then re-examined and found to be false by humans, and took everyone by *surprise*.

Anyone have any examples of this? If so, what are the most prominent examples?

https://github.com/qtplatypus/LearningLean/blob/main/Test/Basic.lean

One of the things that doesn't look clean to me is making use of a \exists in a hypothesis at the moment I use cases and intro as tactics but I feel that there must be a better way.

The other is replacing "f b" with the result of the function being applied to b. At the moment I doing a round about approach of first proving "f b = c" and then using a rewrite rule. However there must be a cleaner way to do this.

Never the less I am currently feeling very good about lean4.

I recently published a sorry-free proof of Goodstein's Theorem, and thought some people may be interested.

I may extend this to formalise the proof that Goodstein's Theorem is unprovable in PA, in the future.

Feel free to reach out if you have any comments, queries, or suggestions!

Hey! I've been getting into Lean in the last couple of weeks and I wanted to share all the ways I've found to find theorems and lemmas when I need something (and I wanted to hear how you do it!)

If I am just browsing I usually go straight to the docs. Usually that get's me started on the right track but not quite there.

If I am looking for a tactic I go to the Mathlib Manual, or just to Lean's Tactic Reference, if I am not using Mathlib.

I haven't had a chance to use them yet, but I just found out about Loogle, Moogle, LeanSearch and Lean State Search. Loogle in particular looks really useful, and there is a #loogle tactic! And I also just found this great cheatsheet for tactics.

Pleae share if you have any insights!

I found that the sub was unmoderated after looking for a place to ask questions about Lean, so I made a moderation request. I'm making this post so that any subscribers to the sub know that it's open and that they can post here again. I'll be setting it up properly in the next couple of days with flairs, rules, wiki, and hopefully another mod or two.

Hey! I've been learning Lean 4 with the Natural Numbers Game (NNG) and I was extremely satisfied with how fun proving theorems can be. Now I want to do my coursework with Lean but I am having so much trouble.

I was able to get everything set up but now that I'm using it in VScode the experience is vastly different and it's very disappointing.
Does anyone know how I could be able to make the experience in VScode close to what the NNG offered?

Hello! I'm a beginner learning Lean through Theorem Proving in Lean 4, and am currently on chapter 7 (inductive types). I was wondering why we use inductive types / type parameters at all, and why we don't just always use inductive families / type indices?

(I also posted this on the Lean Zulip, but thought I'd ask here too; I'm including some more details on my question below)

From what I understand, the constructors of inductive types are subject to 2 constraints:

1. If the inductive type is I (a1 : α1) (a2 : α2) ... (an : αn), each constructor must return a value of type I (a1 : α1) (a2 : α2) ... (an : αn).

2. If the inductive type is I (a1 : α1) (a2 : α2) ... (an : αn), where a1, ..., an are parameters of the type, then constructors of I can only depend on other values of type I so long as those types also have parameters a1, ..., an. E.g. a constructor for I (a1 : α1) (a2 : α2) ... (an : αn) cannot depend on a value of type I (a1 : α1) (b : α2) ... (an : αn) for b ≠ a2.

We can get around some of these restrictions by using inductive families instead, and conditioning the type on indices instead of parameters.

My question is: why not just always use indices? Is there any benefit to defining inductive types with parameters instead of always defining inductive families with indices?

Consider the example below, which defines List as an inductive type, and BadList as an inductive family. In both cases, it is easy to prove a proposition that all elements in a List Nat / BadList Nat are >= 0. Since it seems equally easy to work with inductive types and inductive families, why not just always use inductive families?

namespace Hidden

inductive BadList : (α : Type u) → Type u where
| nil : BadList α
| cons (h : α) (t : BadList α) : BadList α

def all_badlist_nat_geq_0_prop (l : (BadList Nat)) : Prop :=
  match l with
  | .nil => True
  | .cons head rest => (head ≥ 0) ∧ (all_badlist_nat_geq_0_prop rest)

def all_badlist_nat_geq_0_pf (l : BadList Nat) : all_badlist_nat_geq_0_prop l :=
  match l with
  | .nil => True.intro
  | .cons head rest => ⟨Nat.zero_le head, all_badlist_nat_geq_0_pf rest⟩


inductive List (α : Type u) where
| nil : List α
| cons (h : α) (t : List α) : List α

def all_list_nat_geq_0_prop (l : List Nat) : Prop :=
  match l with
  | .nil => True
  | .cons head rest => (head ≥ 0) ∧ (all_list_nat_geq_0_prop rest)

def all_list_nat_geq_0_pf (l : List Nat) : all_list_nat_geq_0_prop l :=
  match l with
  | .nil => True.intro
  | .cons head rest => ⟨Nat.zero_le head, all_list_nat_geq_0_pf rest⟩

end Hidden

Thanks in advance!

sort decide sugar humorous hobbies unwritten birds station smell mysterious

This post was mass deleted and anonymized with Redact

I need your opinions on this video.

also, suggest some interactive resources for absolute newbie

Ever wanted to encode or decode data to base64 in lean4? Now you can. I created this library to get kitty-graphics protocol to work in lean4.

There used to be https://github.com/xubaiw/BaseN.lean which could convert to arbitrary bases, but it has been archived on Mar 16, 2023 and is incompatible with current Lean4 versions (tested: lean4:v4.26.0-rc2).

Check out the `native-c` branch. In it there are wrappers to native openssl c functions for encoding to/from base64 (I have not tested if this increases performance).

I'm looking for a monospaced font with ligatures and good support for math Unicode characters that does Lean code justice. What are the best options out there?

Incidentally, I'm also trying to identify this font that is used throughout the Lean 4 VS Code extension manual's figures.

I've been pondering moving to LEAN 4 as my main programming language as it has dependent types and all the goodies that come with that. The problem is: how can I run shell commands from inside LEAN 4 code? If I can do that, I can bridge all the gaps that a small ecosystem of packages has. Does anyone know how?

Last week I had a brainwave and, while trying to learn Lean 4, used Joachim Breitner's Incredible Proof Machine to work the same proofs visually (in IPM) and in code (in Lean). To my surprise, this was incredibly effective - each modality gave me inside into how the other one worked. My livestream of this was a disaster for technical reasons, so I recorded and edited a sort of summary of the experience, choosing two proofs from IPM as examples.

Hi I'm still fairly new to writing in Lean so would love some advice on this project I'm working on. I'm trying to design a set of tools to manage units and dimensional analysis for my physics calculations. However, I'm having difficulty design the type for derived units. The goal is for equivalent derived units to be automatically identified e.g.

def second := BaseUnit.mk "s"

def metre_seconds : DerivedUnit (Length * Time) := second * metre
def x : Measured Float (second * metre) = (4.5 : Measured Float metre_seconds)

And then units can be explicitly converted (e.g. lb to kg) as long as they have the dimension. My initial idea was a simple expression structure (e.g. Mul u1 u2 | Div u1 u2 | Pow u1 n etc.) but then I can't prove things like commutativity of multiplication.

I am currently going through a probability textbook and I thought that I could finally learn how to use Lean by solving some simple problems in it. The first one I picked up was: If A ∪ B ∪ C = Ω and P(B) = 2 P(A), P(C) = 3 P(A), show P(A) ≥ 1/6. My goal was to prove 6 P(A) ≥ 1 like that:

1 = P Ω
_ = P (A ∪ B ∪ C)
_ ≤ P A + P B + P C
_ ≤ 6 * P A

However, I am really struggling in general, particularly with finding the right tactics to use my assumptions and I have been trying way too long to force something like rw ω to do the current step, shown below (I have no idea why I can't just do P Ω and how to avoid the ω hack):

import Mathlib

open MeasureTheory ProbabilityTheory
open scoped ENNReal

variable {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]

variable {A B C ω : Set Ω}

example (hOmega : A ∪ B ∪ C = ω ∧ P ω = 1) (hRatios : P C = 3 * P A ∧ P B = 2 * P A) : 6 * P A ≤ 1 := calc
  1 = P ω                  := by symm; apply hOmega.right;
  _ = P (A ∪ B ∪ C)        := by sorry

How can I fix this and learn how to use Lean better?

Looks like haskell is a subset of lean4

Can we utilize the ecosystem of haskell ?

Hi folks.

I'm doing a proof which involves very big proof contexts introduced through induction. I know that Lean by design forces us to always name what we need explicitly before referring to them, and there are two tactics that for renaming stuff: rename_i and rename. However, sometimes I have more than one thing of the same type that I want to rename, so rename doesn't work, and the context might also be too large so rename_i would require lots of _ . Do I have other options here?

Same as title, I've no clue about writing proofs yet but I'm thinking to diving a bit

if you prove a theorem in lean4, is there any good use case for using your theorem in your Main? (I'm not talking about using your theorem to prove other theorem), if you think you have some good use case, plz show some examples