ex/flex和yacc/bison编写一个 C 程序，将λ 演算风格的定理证明翻译为希尔伯特公理系统的证明序列。
程序需要：
- 解析类似
function<A,B,C>(h: A->B) -> ...的 λ 项输入； - 利用给定的三条公理模式（A1-A3）和三个可直接引用的定理（H1, H3, H5）；
- 通过演绎定理（Deduction Theorem）和 MP 规则，逐步输出带 LaTeX 排版的希尔伯特风格证明；
- 代码需放置在
src/和include/中，使用 Makefile 管理构建，并遵循 K&R 代码风格。
提供的样例里，除了一个“蕴涵传递”的基本定理，还有两个需要巧妙调用排中律的q1和q2。 而且，测评方还藏了看不到的隐藏用例，想浑水摸鱼是没门的。
给出的 Prompt 任务原文
测试方法
Deepseek 使用官方的 V4 Pro[1M] 模型，接入 Claude Code 命令行工具。Claude 使用 Github Copilot Pro+ 套餐的 Claude Opus 4.7 模型（高达7.5x倍率qwq），接入 VS Code Copilot 插件使用。二者均先在 Plan 模式规划，然后才开始执行。
评分维度与结果
评测从以下五个维度进行打分（满分 100），同时记录了用时和费用。
| 维度 | DeepSeek V4 Pro | Claude Opus 4.7 |
|---|---|---|
| 正确性 (60) | 60 | 60 |
| 构建系统 (10) | 6 | 8 |
| 输出格式遵循 (10) | 5 | 10 |
| 代码质量与格式 (10) | 8 | 8 |
| 异常处理 (10) | 5 | 6 |
| 总分 | 84 | 92 |
| 用时 | 29 分钟 | 15 分钟 |
| 费用 | 2.1 元（API 直调） | 约 2.7 元（订阅点数换算） |
核心能力：正确性齐平，均通过全部测试
在最关键的正确性上，两个模型均拿到了满分。
无论是标准的蕴涵传递（A→B, B→C推出A→C），还是需要巧妙构造排中律的q1、q2，它们都能生成逻辑严密、且通过所有隐藏用例的希尔伯特证明序列。这说明在深层逻辑推理与代码生成能力上，两者都已达到专业开发者水平。
工程细节与格式遵循：Claude 更显“规矩”
差距主要出现在构建系统和输出格式两个维度。
- DeepSeek生成的 Makefile 没有将 flex/bison 生成的
.c文件分离到build目录，未能体现“解耦解析模块与翻译输出模块”的意图；输出证明也未使用示例中的 LaTeX 排版（如$...$），内部引用名称也没有完全对齐样例风格。这些虽然不影响程序的正确运行，但在 “按规范交付” 的要求下被扣了分。 - Claude则严格遵循了所有显式与隐式约定，Makefile 整洁、输出格式甚至与样例几乎一模一样，展现出更好的指令细节遵循能力。
两者的代码风格得分相同（8分），都未能完美实现 K&R 内核风格、部分函数略长，表明在软性编码规范上还有提升空间。
异常处理：均不够“开发者友好”
Claude 的错误信息偏样板，缺少具体错误原因；DeepSeek 的错误信息则缺少行号，定位困难。在实际工具开发中，精确的错误提示对调试至关重要，两项均只能算是“基本可用”。
成本与灵活性：DeepSeek 的显著优势
本次测评最值得关注的反差，体现在使用成本与灵活性上：
- DeepSeek直接通过 API 按量计费，完成一次复杂任务仅需 2.1 元，无需预付费，无每日限额，可随时并发调用。
- Claude的测评费用约 2.7 元，但这是建立在GitHub Copilot Pro+ 订阅（每月 260 元人民币）的基础之上，且该订阅面临暂停新用户注册和限量等问题。实际开发中很可能遭遇用至半途被限流的窘境，且每月无论是否用完都要支付 260 元。若改为直接调用 Claude 官方 API，同等规模的 token 消耗很可能飙升至 15 元以上，成本增加数倍。
对于需要频繁集成调试、批量处理或者构建自动化流水线的个人开发者和小团队而言，DeepSeek 的定价模型无疑是可推广性的巨大优势。
综合评语
- Claude Opus 4.7更像一位经验丰富的“交付专家”：一次生成接近成品，能精准扣住所有格式约束，适合预算充足、追求零修改的直接部署场景。
- DeepSeek V4 Pro则是一名逻辑能力顶尖、但细节上稍显粗犷的“效率先锋”：它在核心正确性上毫不逊色，仅因工程规范与格式呈现被扣分，而这些完全可以通过更精细的提示词（例如预先提供理想的 Makefile 模板、明确要求
$...$排版）轻松补齐。其按量计费、无订阅锁定的高性价比，在长期长尾任务中优势明显。
这次对比清晰地表明：AI 代码助手之争已经不是单纯“能不能做对”，而
)
