7 ms·
I would pay a fairly large chunk of my income to someone working on this kind of alternate representation of mathematics full-time. Email me at soham [at] soh.a
by sohamsankaran 6y ago
I would pay a fairly large chunk of my income to someone working on this kind of alternate representation of mathematics full-time. Email me at soham [at] soh.am if you're interested.
- zozbot234 6y agoThe closest thing to this kind of alternate representation is formal mathematics, as seen in systems like Mizar, HOL Coq, Lean, Isabelle and the like. The fact that it generally "looks like computer code" is often seen as a drawback, but it does have its advantages. In fact, some of these systems allow for constructive theories, which means that they are programming languages of a sort.
- sohamsankaran 6y agoI think there's a place for alternate representations like these outside of proofs that need to be exhaustively machine-checkable. I have, for what it's worth, had far better experiences with Coq and the like than with mathematics in general.
- elbear 6y agoI'm curious, what's your motivation for wanting this? I'm asking because: a) I'd be interested in your offer b) It's not clear how this alternate representation would look like. I'm hoping that your possible use cases would shed some light on that