В работе представлен подход к автоматическому выделению элементарных математических фактов (вида «Предпосылка → Свойство/Объект») из текста с использованием синтаксических деревьев предложений и деревьев выражений для формул. Извлечение фактов осуществляется по эмпирически полученным правилам, учитывающим тип синтаксической связи и семантику слов, с возможностью применения нейросетевых методов. На основе выделенных фактов и связей между переменными в формулах предлагается логически выводить новые факты для проверки непротиворечивости утверждений и достаточности доказательств в тексте.