Yufan Zhao

Stream: new members

[Yufan Zhao]

Hey everyone! I am Yufan, and I just started in an AI research role in April. I have been trying to improve the reasoning and planning capabilities of LLMs, and since last month I've been trying to do it for Math reasoning.

Right now I am looking at the DeekSeek Prover paper (https://arxiv.org/abs/2405.14333) and the miniF2F dataset. At the very last page of the paper in appendix A.4, there is a massive list of import packages that I think contains all possible packages needed for miniF2F. Importing this list of packages manually reduces the burden on LLMs. However, copy-pasting that list gives many "file not found errors".

I suspect the reason is that there has been some refactoring and reorganization in mathLib since the DeepSeek Prover people did their experiments. For example, there is a:

import Mathlib.Algebra.GroupPower.Basic

but that file is not there anymore:

https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Algebra/GroupPower

Is there anywhere I can find these refactoring and reorganization changes?

[Yaël Dillies]

Apologies, I think I am (almost) the sole contributor to these file renames you're hitting. Some renames are mentioned on the #blog but I can't really expect you to click through a hundred links to figure out what happened. We're still missing an automated tool here...