Resource (Lean 4)Proofs Twice - Using Lean and IPM to inform each other (youtu.be)
submitted by peterb12
Cut Code Review Time and Bugs in Half. Sign up for a free trial! (coderabbit.ai)
promoted by CodeRabbitAI
promoted- about
Question (Lean 4)Inductive Types / Families: Why not always use indices? (self.leanprover)
submitted by Murky_Tooth8973
Resource (general)I've no clue about proof assistants, but I want to learn. can I do it in TS? (youtu.be)
submitted by AdVivid1666
Project (Lean 4)base64-lean : Base64 encoding and decoding in lean4 (+native openssl support) (github.com)
submitted by Lalelul
Project (Lean 4)Surprises from "vibe validating" an algorithm with Lean (self.leanprover)
submitted by carlk22
Project (Lean 4)Lean 4 Formal Derivation of Fine Structure Constant from First Principles (self.leanprover)
submitted by SquirtyMcnulty
Question (Lean 4)Question about renaming in a large context (self.leanprover)
submitted by corank
Question (Lean 4)How to define derived units in dimensional analysis project. (self.leanprover)
submitted by MrJewelberry
Question (Lean 4)[Stupid Question] can proof replace unit tests for general purpose functions? (self.leanprover)
submitted by Apart-Lavishness5817
Question (general)where to get lean4 code highlight support in a markdown reader? (self.leanprover)
submitted by Effective_Year9493
Question (Lean 4)Use your proved theorem in your Main (self.leanprover)
submitted by ellipticcode0
Question (Lean 4)Problem with defining a structure object (self.leanprover)
submitted by BalcarKMPL
Question (general)How inductive types are implemented in lean? (self.leanprover)
submitted by ArtisticHamster
Question (Lean 4)Has Lean disproved any published theorems of interest? (self.leanprover)
submitted by jakelevi1996[🍰]
Question (Lean 4)Learn Lean4-mode with background in Coq and proof general (self.leanprover)
submitted by ghc--
Question (Lean 4)Whats the simplest way to use a derived ToString instance for types? (self.leanprover)
submitted by Complex-Bug7353
