|
|
|
|
|
|
by lioeters
5 days ago
|
|
|
Automath is also an early example. > Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness. |
|
|