今天这篇是把墨尔本大学一位计算机方向 Professor 的公开页面整理一遍。文章不展开判断，也不替导师做招生承诺，目标是把一个申请者在递交研究计划之前，至少应该核对清楚的入口和细节列出来。导师姓 Kaliszyk，所在的是 School of Computing and Information Systems。和他相关的几条公开信息——包括 2025 年的国际基金、显示在邮件列表里的 PhD 招生帖子、以及个人主页上长期更新的论文清单——都可以从外部页面直接核对。
一、导师与所在学院的公开信息
Kaliszyk 教授目前在墨尔本大学计算与信息系统学院。学院的整体定位偏综合，研究方向覆盖人工智能、计算机科学、人机交互和信息系统四块。学院的 Head of School 在公开页面里写到，全院规模约 500 名教职员工和 8000 名学生，下设多个研究组。对申请者来说，这一点的实际意义是：同一座学院里候选导师不止一位，Kaliszyk 教授只是其中专门做形式化方法和自动推理方向的代表之一，研究计划完全围绕他的工作来准备，也可以同时把同学院其他相关研究组列入备选名单。
他本人的学术轨迹在公开 CV 上写得比较完整：早期在荷兰 Radboud University 完成博士，之后在德国慕尼黑工大、日本筑波大学有过博士后和访问经历，再之后长期在奥地利 Innsbruck 大学任教，最近正式加入墨尔本大学并担任 Professor。这一段履历里值得申请者留意的是，他的合作网络还覆盖捷克技术大学等欧洲机构，论文署名经常出现 University of Innsbruck 和 Czech Technical University in Prague 的双地址。这意味着研究组的学术资源不只在澳洲一地，但具体合作机制是否会延伸到 PhD 学生，需要在套磁阶段直接确认，不能仅凭论文署名做推断。
二、研究组主要在做什么
从他个人主页和近三年的会议论文看，研究组的主线可以拆成三条。第一条是自动定理证明本身，也就是给计算机系统配上更强的推理能力，让它能在数学和形式系统里自动找到证明。第二条是把机器学习的方法嵌进证明流程里，让模型从已有证明中学习选择策略，再去引导新的证明。第三条偏交叉，是与交互式定理证明器（Coq、Isabelle、HOL 这一类工具）结合，让数学家可以在更高的抽象层面工作。
用普通申请者的话讲，这条线的研究问题大致是：当一个数学命题或工程规约写成形式语言之后，能不能让算法自己找出一条可以被机器逐步验证的证明路径，并且在面对新问题时表现得比传统启发式更稳定。这类工作离应用并不算远——例如区块链智能合约的形式化验证、关键软件的安全性证明，都是它的下游场景。如果硕士阶段做过定理证明、形式语义、SAT/SMT 求解器、强化学习或符号-神经混合模型，理解这些论文会更顺。
三、最近一年值得读的几条公开成果
进入 2025 年之后，他名下比较显眼的一条公开消息是参与一项名为 DEEPER 的国际合作项目，由 AI for Math Fund 提供约 100 万美元（约合 150 万澳元）的资助，合作方是布拉格捷克技术大学的两位研究者。项目本身的描述是开发面向自动推理系统的 AI 引导方法，并把它整合进现代证明助手。这条信息可以从墨尔本大学官方新闻页面直接核对，是目前最容易确认的资助来源。
在论文层面，他在 2025 年的 IJCAI、CICM、FroCoS、CPP 等会议上有多篇合作论文出现，主题集中在重写系统的策略合成、高阶集合论证明 hammer、Coq 证明模式挖掘等方向。这些会议本身就是形式化方法和AI 辅助推理的主舞台，因此论文记录在 dblp、ACM Digital Library、Google Scholar 上都能查到。申请前没必要把论文都读完，挑两三篇标题最贴近自己背景的看摘要和实验设置就够，目标是判断自己写出来的研究计划能不能接得上他最近的研究语言。
四、博士项目入口与可核对的招生信息
墨尔本大学的工程与信息技术博士项目对应的是 Doctor of Philosophy – Engineering and IT，申请入口在 study.unimelb.edu.au 的 graduate research 页面。校方对所有 PhD 申请者会做统一的研究背景和导师匹配审核，因此即使是想跟 Kaliszyk 教授读，也需要走全校 PhD 招生入口，并在网申阶段写清楚目标导师和研究方向。
Kaliszyk 教授本人在 2025 年初通过 hol-info 邮件列表公开过一条招生帖子，写明研究组在墨尔本招收多名 PhD（graduate researcher）名额，方向集中在自动推理、形式化证明和学习辅助证明指引。帖子要求申请者具备形式化证明、机器学习或自动推理方向的背景，本科或硕士需要计算机或数学相关学位。需要说明的是，邮件列表帖子只能作为弱信号，不能直接等同于 2026 年仍然有名额。如果递交申请前没有看到更新过的招生页面，建议在套磁邮件里直接询问当年是否仍有 opening。
奖学金部分以学校官网最新页面为准。墨尔本大学的 Research Training Program (RTP) Scholarship 是较常见的全奖路径，覆盖学费和生活补贴；除此之外学校还提供 Melbourne Research Scholarship 等校内奖学金，金额与名额随年份调整。这一点不在导师可控范围内，所以套磁阶段不必把奖学金的承诺写进邮件，只需要表明自己愿意申请校内奖学金、并且符合资格条件即可。
五、申请前的准备清单
比起立刻动笔写研究计划，更建议先做三件事。第一是把他个人主页 ckaliszyk.github.io 上 2024–2025 年的论文标题逐条扫一遍，在每条论文旁边写一句自己能不能看懂、自己有没有相关经验，这一步会决定研究计划的真实可行度。第二是看墨尔本大学计算与信息系统学院的 PhD 申请页面、招生时间线和材料清单，把申请窗口期、推荐信数量、英语语言成绩要求记下来，避免临近 deadline 才发现卡住的细节。第三是检查自己的本科或硕士成绩单上有没有数理逻辑、离散数学、编程语言原理、机器学习基础这几门课的痕迹，如果都没有，研究计划里至少要写清楚自己打算如何补齐这部分基础。
套磁邮件可以保持简短：自我介绍两到三句，列一两段过往与形式化方法或自动推理相关的项目经验，再提一篇你认真读过的他的论文并写出一个具体问题。直接问今年是否仍有 PhD 名额、是否欢迎邮件附上 CV 和研究兴趣，比拐弯抹角更有效。邮件里不要出现「如果可以请帮我推荐」这类与正式申请流程不符的请求。
六、什么样的背景更容易接住这条线
更适合重点关注他研究组的，往往是几类背景：本科或硕士主修计算机科学或数学，对数理逻辑、λ 演算、类型论或编程语言语义有过课程或项目接触；做过 SAT/SMT 求解器、Lean/Coq/Isabelle 证明助手、或机器学习与符号系统结合的小项目；以及虽然不是直接做形式化方法，但在工程上做过代码静态分析、程序合成或软件验证方向的同学。
另外还有一种情况比较模糊：本科是数学系、对算法和编程比较熟、但没有写过证明助手相关代码。这类同学并不是没机会，但研究计划里需要更明确地说明，自己打算用哪段时间补哪些工具，以及为什么相信这条路径走得通。比起空泛地表达兴趣，给出一个能验证的小目标更能说服人。
七、信息来源与阅读建议
本文整理时主要参考了以下公开页面：墨尔本大学 Find an Expert 的 Cezary Kaliszyk 主页、his 个人主页 ckaliszyk.github.io、墨尔本大学官方新闻关于 AI for Math Fund 的报道、墨尔本大学 study.unimelb.edu.au 的 PhD 申请入口、ACM Digital Library 与 Google Scholar 的公开论文记录、以及 hol-info 邮件列表中 2025 年初的招生帖子。所有提到的资助金额、招生信息、奖学金条款，都建议申请前再去对应官方页面确认一次，再决定要不要把这位教授放进自己的导师候选名单。
本文仅基于公开资料整理，不代表学校、院系或导师官方招生承诺。奖学金、申请要求和导师招生情况可能随年份变化，请以学校官网和导师最新回复为准。
