Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
alphabetr
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
3 ms
·
1.
▲
by
alphabetr
4y ago
> Higher level math would be an order of magnitude easier with machine checked syntax. This just isn't true, at least in terms of developing new mathematical ideas. There are already tools (e.g Coq) for providing mathematical syntax
2.
▲
by
alphabetr
4y ago
I get the feeling that you're stuck in Terry Tao's 'rigourous phase' of mathematical understanding, where everything in the end is a computation and has to be carried out according to a set of rigorous steps and definiti