Des chercheurs de l'Université de la ville de Hong Kong, de l'Université Sun Yat-sen, du laboratoire Huawei Noah's Ark et d'autres institutions ont proposé un cadre de synthèse de données de raisonnement mathématique unifié MUSTARD, qui peut générer de grandes quantités de données de raisonnement mathématique de haute qualité, correctes, lisibles et compréhensibles par l'homme.Cet ensemble de données est l'ensemble de données open source MUSTARDSAUCE pour la recherche.Chacune de ces données contient la description du problème et la solution en plusieurs étapes en langage naturel, ainsi que la description du problème et la solution en plusieurs étapes dans le langage formel double Lean 3. Les données MUSTARDSAUCE comprennent des problèmes de mots mathématiques et des problèmes de preuve de théorèmes, couvrant les niveaux de difficulté de l'école primaire à l'enseignement supérieur. Le nombre d’étapes de raisonnement dans une question augmente à mesure que la difficulté de la question augmente. Le problème le plus difficile nécessite environ 30 étapes à résoudre, soit environ 20 tactiques Lean 3.