|
|
|
|
|
by hxypqr
915 days ago
|
|
I haven't looked at the code, but I wanted to ask in advance if it is possible to incorporate lean4's formal mathematical capabilities into the current architecture to obtain more precise answers when processing mathematical PDF documents. For example, to implement something similar to the functionality described in terrytao.wordpress.com/2023/02/18/would-it-be-possible-to-create-a-tool-to-automatically-diagram-papers/. |
|