top | item 46744611 (no title) erichocean | 1 month ago Getting the AI to work with Rocq is a useful goal, Lean has been useful so far. discuss order hn newest benreesman|1 month ago I mostly write lean4 now and emit proof-carrying System F Omega via rfl. It's the right level of abstraction when the droids have been pinned to theory laden symbolisms. It's also just pleasant to use.
benreesman|1 month ago I mostly write lean4 now and emit proof-carrying System F Omega via rfl. It's the right level of abstraction when the droids have been pinned to theory laden symbolisms. It's also just pleasant to use.
benreesman|1 month ago