快手科技 发布 Leanabell-Prover 数据集 数据集, 应用在 自动化定理证明、机器学习 领域

快手科技 本次发布的数据集 Leanabell-Prover 数据集, Leanabell-Prover数据集是由快手科技的研究团队创建，包含约152万条形式化语句，以及22万条带有详细非正式评论和验证证明的形式化语句。该数据集用于持续训练和强化学习，以提高自动化定理证明器在 Lean 4 语言中的性能。数据来源于多个项目，包括标准的 Lean 4 数学库Mathlib4、Lean Workbook、Goedel-Prover 和 STP 等合成定理，以及通过PromptCoT 框架合成的数学问题。数据集旨在解决自动化定理证明中形式化语言与自然语言之间的差距问题，推动数学证明生成领域的进展。

查看Leanabell-Prover 数据集

README 内容： 

关于 快手科技 , 快手科技（Kuaishou）是中国领先的短视频平台之一，成立于2011年，总部位于北京。公司通过其平台快手和快手极速版，为用户提供短视频创作、分享和观看服务，是中国数字娱乐行业的重要参与者。

关于 arXiv , arXiv 是一个免费分发服务和开放获取的学术文章档案库，涵盖了物理学、数学、计算机科学、定量生物学、定量金融、统计学、电气工程和系统科学以及经济学等领域。该网站上的材料并未经过 arXiv 的同行评审。