本讨论班面向北京大学数学科学学院大二、大三本科生，与夏壁灿教授、林作铨教授联合开设。

时间：每周一下午5-6节，13:00-14:50。

地点：TBD。

本人所承担内容：可从如下题目中任选其一：

1）《The method of coalgebra: exercises in coinduction》

共代数作为基于状态系统的理论模型，在计算机科学中已经得到了广泛应用。通过阅读本书，可以学习范畴论、共代数相关的基本理论和共归纳推理与证明方法，选择该问题的同学需具有较好的代数基础，在讨论班阅读本书并轮流报告，报告结束后感兴趣的同学可对某一相关问题（信息物理系统的共代数模型、神经网络的共代数模型、量子共代数等）开展研究。

2）基于深度学习的智能化定理证明 当前交互式定理证明工具中证明过程的构造很大程度上依赖于和用户之间的人机交互，需要用户指导证明的构建过程，近年来定理证明的自动化已经成为人工智能领域的研究热点之一。通过机器学习方法，可以使得定理证明器根据证明目标生成合适的证明过程步骤，从而提高定理证明的自动化程度。对机器学习、深度学习等技术在定理证明中应用感兴趣的同学可以选择该问题进行研究。选择本问题的同学需已有一定的相关知识基础（机器学习、深度学习、神经网络）并具有较好的编程能力。

3）区块链智能合约的形式化建模与验证 以去中心化为核心的区块链技术近年来随着虚拟货币的热潮迅速进入大众视野，而虚拟货币与现实货币的关联使得区块链的任何安全隐患都可能导致极其严重的后果。由于以太坊本身及其开发者所编写智能合约中的错误及漏洞，已经导致了多起造成巨大经济损失的区块链攻击事件，因此采用形式化验证技术保障智能合约的可靠性至关重要。以太坊官方已经成立了专门的形式化研究部门，并且和形式化方法研究人员开展了密切合作。对区块链、智能合约技术感兴趣的同学可选择该问题进行研究，通过使用定理证明器及约束求解工具对智能合约进行形式化验证，要求选择该题目的同学需具有较好的编程能力。