图片中左侧的女人名字是Sara Negri，欧洲科学院院士，右侧的男人名字是Jan von Plato，是Negri的老公，芬兰逻辑学泰斗，拿过ERC Advance Grant，是顶级研究资金资助，但是似乎还没有他老婆的欧洲科学院院士名头响亮。

他们手上拿的是Oiva Ketonen在1944年二战期间的博士毕业论文复刻版，深入研究矢列演算系统里无收缩规则的G3系统的特性的，Ketonen被认为是Gentzen系统的最重要的继承者，对Negri和von Plato的工作起到了重要的承前启后的作用。

----

证明论领域的学者其实是很吃亏的，因为研究领域太小众，没机会拿诸如诺贝尔，菲尔茨这样的大奖；不仅是Negri和这样的大奖无缘，有着法国科学院和欧洲科学院双院士头衔的Girard也没有，Coq的发起者Coquand也没有，再往前Skolem，Gentzen，Prawitz这些奠基者也没有，Per Martin Lof的运气好一些，拿到了Rolf Schock奖，Kolmogorov奖章，瑞典皇家科学院和欧洲科学院两院院士。

但正是这些人的工作，奠基了现代证明论，让AI在未来有可能突突掉人类选手，解决难度超过菲尔茨奖获得者们曾经解决过的那些问题。