looks like Lean is popular today, so here's a little post on how/why it works and implementing a mini version of it in Julia

you don't really need to know Julia for this since it's very simple! (and you _definitely_ don't need to know Lean)

anyways, here's the post

if you're more of a livestream enjoyer:

@outputlayer rosé pine dawn (no italics), font is berkeley mono from the inimitable @usgraphics

@frang_u99393 oh yeah, dependent types fully show up here, then Lean would be an easy side effect of the type system with some additional niceness in that you can actually write software in Julia

@frang_u99393 "Lean" as a stand-in for "Lean-like interactive theorem proving systems"