FVSpec: Real-World Property-Based Tests as Lean Challenges

FVSpec 从真实 Python 仓库抽取 property-based tests，再转换为 Lean 4 specification challenge，目标是把工程测试里的性质变成形式化证明任务。它的贡献重点在数据来源：不是手写数学题，而是从实际软件仓库中提炼行为约束。这个方向值得关注，因为 property-based tests 天然携带输入空间和不变量，比普通单元测试更接近 Lean 里可证明的 specification。