I built the RealWorld app in Lean 4

(leangineer.com)

1 points | by saviorand 4 hours ago ago

1 comments

  • saviorand 4 hours ago ago

    I wanted to know if Lean 4 is usable for an everyday web app yet, not just for proofs, so I built RealWorld (the Medium clone) in it, frontend included, using Datastar. Looks like it's feasible now with the new libraries. This post describes the experience