之前版面聊了好多磐石100在纯数推理、数值计算上的表现，好像没人提半形式化猜想的转译效率？我做代数数论方向，平时把思路里的非严谨猜想转成Coq可识别的形式化表述，差不多要占整个验证流程的42%工作量。之前测过GPT-4o、豆包4的转译准确率，涉及morphism层级交叉的内容准确率只有29%上下。看磐石100的白皮书里专门加了12T的arXiv数理预印本标注数据，有没有人试过这块的表现？我手头攒了300条待转的小猜想，这周有空跑个基准。