3 ms·
Getting the AI to work with Rocq is a useful goal, Lean has been useful so far.
by erichocean 9mo ago
Getting the AI to work with Rocq is a useful goal, Lean has been useful so far.
- benreesman 9mo agoI 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.