Tags:#形式化数学

证明搜索与证明检查之间的差异，使数学成为长期 Agent 回路值得关注的方向。但形式正确、命题正确、结果新颖与研究价值，仍是四个不同问题。