Machine Learner for Automated Reasoning (MaLARea) is a learning and reasoning system for proving in large formal libraries where thousands of theorems are available when attacking a new conjecture, and a large number of related problems and proofs can be used to learn specific theorem-proving knowledge. The last version of the system has by a large margin won the 2013 CASC LTB competition. This paper describes the motivation behind the methods used in MaLARea, discusses the general approach and the issues arising in evaluation of such system, and describes the Mizar@Turing100 and CASC'24 versions of MaLARea.

翻译：自动理性机器学习者(MaLARea)是一个学习和推理系统,用于在大型正规图书馆进行验证,在大型正规图书馆中,有数千个理论在攻击新猜想时可用,大量相关问题和证据可用于学习具体的理论证明知识,该系统的最后一个版本在2013年的CASC LTB竞赛中大获成功,本文描述了在MaLARea使用的方法背后的动机,讨论了在评价这种系统时采用的一般方法和出现的问题,并描述了Mizar@Tring100和CASC'24版的MaLARea。