InternLM 发布 Lean-Github 数据集, 应用在 形式化数学、机器学习 领域

InternLM 本次发布的数据集 Lean-Github, 我们发布了Lean-Github和InternLM2-Step-Prover，这两个资源包括从100多个Lean 4仓库编译的29K定理，以及在Lean-Github和Lean-Workbook上微调的7B模型。该模型在MiniF2F-test、ProofNet和Putnam问题上展示了最先进的性能。

查看Lean-Github

Dataset card 内容： 

Files and versions 内容： 

关于 InternLM , InternLM 是由上海人工智能实验室主要开发，专注于开源高质量大型语言模型及全栈开发应用工具链的组织。

关于 HuggingFace , Hugging Face是一个机器学习社区协作平台，专注于模型、数据集和应用程序的创建、发现和协作。该平台支持多种数据类型，包括文本、图像、视频、音频和3D数据，并提供开源工具和付费计算及企业解决方案。