Digital mathematics
Last updated
Last updated
seems very good as a replacement of plain text, because every expression has a canonical representation (just like plain text).
Then, you can use (the version which is a haskell library is quite efficient), to define operators that act on dhall expression (or plain text). This allows you to provide scientific meaning to dhall expressions, for instance define "equivalencies", "simplifications" of expressions. This is now specially relevant because there is a programming language which is essentially based on simplifying mathematical expressions. This is not due to some taste preferences, but because it is a rare (if not unique) way to scale automatically a computation task to massively parallel computation. Until last year, there was a consensus that neural networks were an efficient way to use massively parallel computation. But, open-source, small "thinking" LLMs such as are much better then the traditional use of neural networks (see also , for a robotics context where further progress is also being done using more serial processing, not more parallel processing). The problem however is that these "thinking" models do not scale automatically to massively parallel computation. Moreover, Mathematics is now mostly digital. Because it is now viable to create a good automatic verification of mathematical solutions to mathematical problems all written in traditional mathematical language (using, for instance a translation from natural language to naproche (using a small LLM) , then from naproche to Isabelle and then to Metamath (using existing traditional software). Using such automatic verification, it is possible to create a game environment where a generator of solutions is optimized. So, humans will mostly use dhall-style notation for science (because Mathematics is now mostly digital). And software will mostly use dhall-style notation (everywhere, not only as a user interface) because of the constraints of massively parallel computation. Since I am a Physicist, there is an algorithm from 2017 that connects all of this to Physics, and in particular to my work . This explains my interest in all of this.