3 ms·
If you want something like surreal numbers (or anything that might use ordinal induction) you might be better off with a proof assistant. Lean is being develop
by afiori 7y ago
If you want something like surreal numbers (or anything that might use ordinal induction) you might be better off with a proof assistant.
Lean is being developed specifically for being applicable to math researcher.
- igravious 7y agoProof assistants are too esoteric for me. Coq, Idris, Agda, Lean, way above my pay-grade. Fair play to people that understand them but I can't. It's tough to admit such a thing on a forum like this but there you go. The closest I think I'll need to go along that route is to graft microkanren into a toy language as part of its type system.