The next meeting of the seminar will be held on July 8 at 6 pm (UTC+7) in room 4109 of NSU. Pay attention: the room has changed. You can also connect to the seminar online: https://us02web.zoom.us/j/9421270845. And to be the first one to know about the announcements of upcoming seminars, join the seminar's telegram chat: https://t.me/joinchat/iH16ONtr7zZiZTJi
Topic: Processing of mathematical texts
Speaker: Alexander Perepechko (Moscow)
Automation and verification systems for mathematical proofs work from the bottom up: from basic building blocks to more complex statements, created almost by hand. Is it possible to go "top down": from the corpus of mathematical texts along the path of gradual, albeit partial, formalization? Is it possible to search for statements not by keywords, but by logical meaning?
We propose to discuss possible approaches to such a task, their feasibility, as well as existing tools in this area.
For example, from a linguistic point of view, a mathematical text consists of relatively standard constructions, has little variability and is devoid of most means of expression and many types of uncertainty. At the same time, mathematics is the largest field in which deep semantic analysis is applicable. These features allow us to hope for the productivity of linguistic analysis of mathematical texts to find logical relationships and formalize evidence.
