Hacker News Reader

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.

View on HN

The 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.

I 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.

I'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

Reply on news.ycombinator.com