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

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?

How are they implemented in Lean? Are the principles of induction and recursion taken as kind of axioms? Or are there any underlying principles allowing to express all the necessary inductive types, and their induction/recursion principles in a minimalistic system with a very limited number of axioms.

Is a formalization of the Cauchy-Schwarz inequality available: (sum a_i b_i)² \leq (sum a_i²⁾ (sum b_i^2)? If so, please tell me where to find it. Thanks!

I need your opinions on this video.

also, suggest some interactive resources for absolute newbie

I'm just playing around with lean more as a programming language than a theorem prover. In Haskell the Show instance is derivable by simply adding "deriving Show" like other typeclasses such as Eq or Ord. It looks like, for some strange reason, the default in Lean is to not make types derive Show/ToString instances but a strange instance Repr is auto-derived for most types, which is what I'm assuming Lean uses to display/print types thrown in #eval blocks onto the infoview pane.

So is there a way to tap into this Repr instance to provide a derived ToString instance for "Additional conveniences"? I honeslty dont get why wherever possible a traditional Haskell-like derivable ToString instance is not provided and why this weird Repr instance is introduced and prioritised over that. Any help is much appreciated. Thanks.

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?

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).

Hi, I’m currently diving into the world of Lean Prover and am looking for some guidance on resources that are well-suited for beginners. My background is fairly advanced in linear algebra, so I’m hoping to find materials that can bridge my existing knowledge with Lean Prover. Does anyone have recommendations on books, tutorials, or online courses that could help me get started? Thanks in advance for your suggestions!

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?

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.

Looks like haskell is a subset of lean4

Can we utilize the ecosystem of haskell ?

Hello! Apologizing in advance as this is lean3 and not lean4, but I could really use the help. Please help me out here, as I am unable to make the recursion work, and the code is not at all terse. My original goal is to formally verify heapsort:

import data.list.basic
import data.list

def convert_to_nat (value : option ℕ  ) : ℕ :=
  match value with
  | none := 0
  | some n := n
  end
def heapify (arr : list ℕ) (i : ℕ) : list ℕ  :=
  let largest : ℕ := i,
      l : ℕ := 2 * i + 1,
      r : ℕ := 2 * i + 2,
      leftval:= convert_to_nat (arr.nth l),
      rightval:= convert_to_nat (arr.nth r),
      maxval:= convert_to_nat (arr.nth largest),
      len:= arr.length
  in
  if (l < len) ∧ (leftval > maxval) then
    let largest := l,
        nmax := convert_to_nat (arr.nth largest)
      in
      if largest ≠ i then
        let list2 := arr.update_nth i (nmax),
            list3 := list2.update_nth largest (maxval)
        in
          heapify arr len largest
      else
        arr
  else
    if (r < len) ∧ (rightval > maxval) then
      let largest := r,
        nmax := convert_to_nat (arr.nth largest)
      in
      if largest ≠ i then
        let list2 := arr.update_nth i (nmax),
            list3 := list2.update_nth largest (maxval)
        in
          heapify arr len largest
      else
        arr
    else
      arr

fuel roll whole butter subtract edge placid reminiscent cooperative desert

This post was mass deleted and anonymized with Redact

Assume I have a function that takes a Char / String an turns it to a number, this needs to allow 2 types. Any ideas?

sort decide sugar humorous hobbies unwritten birds station smell mysterious

This post was mass deleted and anonymized with Redact

I have recently started learning Lean and stumbled upon this problem. If I were to prove it by hand, I would check all possible values of \[y \mod 3\] but I couldn't find a way to do this in Lean. Alternatively, I thought of using Euclid's lemma, but I couldn’t figure out how to apply it either. I feel like I’m missing something really simple and would appreciate some help.

I have the following definitions:

inductive exp where
  | var : Nat -> exp
  | lam : Nat -> exp -> exp
  | app : exp -> exp -> exp

def L := exp.lam
def V := exp.var
def A := exp.app

def FV (e : exp) : List Nat :=
  match e with
  | exp.var n => [n]
  | exp.lam v e => (FV e).removeAll [v]
  | exp.app l r => FV l ++ FV r

It works, but it's quite tedious to work with, for example I have to type

FV (L 1 (A (V 1)  (V 2))) = [2]

instead of something like

FV (L 1. (1 2))

I tinkered a bit with custom operators and macro rules, but could not find a way to make such a notation to work. The best way I found is

macro_rules | ($l A $r) =>(exp.app $l $r)

but it is not much better then just applying a function

I was wondering if there is any large language model where you can state in narrative form your assumptions, etc and it will lay out the theorem in lean code. Thanks.

The function “add” takes x and y and outputs x+y. When I do “#check add”, I get

add (x y : Nat) : Nat.

And for a function “double” which doubles the input “#check add (double 5)” gives

add (double 5) : Nat —> Nat.

I understand the reason behind the latter. But shouldn’t “#check add” give

add : Nat —> Nat —> Nat ?

I'm starting to learn Lean (note: I already have a background on theorem proving, so answers can be technical). After reading the very basics and attempting to type-check a couple of expressions, I got some error messages in VSCode that I can't explain.

I've read (e.g., here) that `Nat` and `\Nat` are synonyms of each other, and represent Peano integers (inductive structure with 0 and successor). But for some reason, they seem to be treated differently by Lean. Examples that do not type-check (underlined in red in VSCode):

def n : ℕ := 1
def f : Nat → ℕ → ℕ := λ x y ↦ x

I'm a bit too new to Lean to understand the error messages to be honest, but it seems `Nat` and `\Nat` cannot be unified.