本项目用 Lean4 形式化验证一个红蓝选择问题中的理由结构。项目关注的不是玩家实际会如何选择，而是： 在给定价值准则、背景条件和理由生成规则下，某个策略是否能够成为某个玩家的最终合理策略。