Lean 的基础究竟是什么：读 Hales 的文章之后

2026 年 10 月 9 日，Thomas Hales 在《What’s new》发表了一篇关于 Lean 可靠性的客座文章。 最近围绕形式化数学的讨论，大多在问 AI 已经会证明什么、还能证明什么。 Hales 把问题往下追了一层：我们用 Lean 检查证明，又凭什么相信 Lean？

这个问题值得认真回答。尤其是文章提到，Lean 类型论中的一些基本性质仍没有完整证明， 其中甚至包括“一个项的类型在定义相等的意义下唯一”。 对习惯了数学教材写法的人来说，这很难不令人意外：如此基本的事情，怎么会还没有解决？

但如果读完文章，只剩下“Lean 的地基可能有问题”这一印象，也会错过重要的区别。 一份关于类型论的证明有缺口，与已经从类型论的规则推出矛盾，是两回事。 一个检查器有了可靠性证明，与整套抽象理论的所有重要性质都已证明，也不是一回事。 Hales 的文章把这些问题提到了台前；本文想接着往下讲，说明它们各自是什么， 现有结果究竟证明了什么，以及研究者正在怎样补上缺口。
Continue reading →

Errata

Local theta correspondence between supercuspidal representations, Ann. Sci. Éc. Norm. Supér, 2018

  1. Corollary 5.11, \Gamma+\mathfrak g_{x,r^+} should be \Gamma+\mathfrak g_{x,-r^+}. The proof was correct.

Invariants and K-spectrums of local theta lifts

  1. The condition (\dagger) (on page 180) should also include the case when (G,G') = (\mathrm{Sp}_{2n}(\mathbb C), \mathrm{O}_{4n}(\mathbb C)) and \rho is the trivial representation. In fact, in this case \Theta(\rho) has two irreducible constituents (See “Lee Soo Teck, Zhu Chenbo, Degenerate principal series and local theta correspondence III”).

Generic Hecke algebra and theta correspondence over finite fields

  1. In Theorem 1.1 (eq. (1.8) on page 5; restated in Section 5.4 on page 35), c(\pi) should be 2c(\pi): the conservation relation should read n_{\mathcal{V}'_V}(\pi) + n_{\widetilde{\mathcal{V}}'_V}(\pi) + 2c(\pi) = 2\dim V + \delta, which is exactly what the proof in Section 5.4 yields.

Emacs configuration of Atlas

The following is the steps to add the lexical highlighting of atlas codes in emacs.

  1. Copy “atlas.el” from atlas-scripts:
cp atlas.el ~/.doom.d/
  1. add the following lines in the initial file “~/.emacs”
(add-to-list 'load-path "~/.emacs.d/" )
(load "atlas")
(add-to-list 'auto-mode-alist '("\\.at\\'" . atlas-mode))
  1. Load any “.at” file and enjoy the highlighting.

2022 天元表示论讨论班

本页为 2022 年 5–7 月天元表示论讨论班的历史存档。报告以约化群表示论的前沿技术为主题，采用线上系列专题报告形式；下表保留原报告摘要、海报与录像链接。

Date Time Speaker Title Abstract Host
2022/05/06 15:00-16:30 陈阳洋 Schwartz homologies of Nash groups, part I In this talk, we will give a brief introduction to the Schwartz induction theory of almost linear Nash groups. Poster@XMU
2022/05/13 15:00-16:30 陈阳洋 Schwartz homologies of Nash groups, part II Same as the above. Poster@XMU
2022/05/20 15:00-16:30 陈阳洋 Schwartz homologies of Nash groups, part III Same as the above. XMU
2022/05/27 15:00-16:30 陈哲 Higher Deligne-Lusztig theory I (I) In the first talk I would like to give an introduction to Deligne–Lusztig theory of reductive groups over finite fields, with a focus on the case of SL_2(F_q). Time permitting, I will also discuss some basics of the generalisation for reductive groups over discrete valuation rings (called higher Deligne–Lusztig theory). XMU
2022/06/03 15:00-16:30 陈哲 Higher Deligne-Lusztig theory II (II) In the second talk, I would like to discuss the algebraisation problem of higher Deligne–Lusztig representations raised by Lusztig, which seeks algebraic realisations (via, say, Clifford theory) of these geometrically constructed representations. I will discuss our resolution of this problem at even levels in a joint work with Stasinski in 2017, as well as our recent progress towards the odd level case. XMU
2022/06/10 15:00-16:30 陈哲 Higher Deligne-Lusztig theory III (III) In the third talk, I plan to discuss a curious restriction-to-torus formula of Deligne–Lusztig characters, which is motivated by a phenomenon appeared in the algebraisation problem and by a work of Reeder. XMU
2022/06/17 15:00-16:30 聂思安 Lusztig’s map from conjugacy classes of the Weyl group to the unipotent classes For a connected reductive group over an algebraically closed field, Lusztig constructed a miraculous map from the conjugacy classes of the Weyl group to the unipotent conjugacy classes. We will discuss various interesting properties and applications of the map. Part of the talk is based on joint work with Jeffrey Adams and Xuhua He. XMU
2022/06/24 15:00-16:30 聂思安 Counting points on Newton strata and a multiplicity-one phenomenon Affine Deligne-Lusztig varieties play an important role in the theory of Shimura varieties. Their geometries are controlled by the Newton strata in Iwahori double cosets. In this talk, I will report a multiplicity-one phenomenon on the Newton strata of a large class of Iwahori double cosets, namely, these strata form a stratification and each of them is nonempty and irreducible. We prove it by counting rational points on the Newton strata. As a consequence, we show the corresponding affine Deligne-Lusztig varieties are explicit unions of classical Deligne-Lusztig varieties of Coxeter type. This is based on joint work in progress with X. He and Q. Yu. XMU

2020 Fall Seminar on real reductive groups

This semester, 2020 Fall, we will focus on the representation theory of real reductive Lie groups.
Throughout these seminar talks, we hope to clarify the current status of the subject and stimulate collaborations. We expect the speakers to explain the technical details. The audiences are encouraged to interrupt the speaker and raise questions/make comments. Most lectures will be given in Chinese.

Click the title for the videos of the talks.

Time Conference Id Speaker Title Abstract Host
2020/09/02 NA 董超平 Towards the classification of Dirac series for real classical groups Prof. Dong will collect the math ingredients pertaining to the classification of Dirac series. In particular, he will mention its relation with unipotent representations. SJTU
2020/09/25 2pm-4pm NA 白占强 Gelfand-Kirillov dimensions and associated varieties of highest weight modules In this talk, I will give some introduction to Gelfand-Kirillov dimensions and associated varieties of highest weight modules of Lie algebras (groups). Then I will talk about our work on GKdim and Associated Varieties of highest weight (Harish-Chandra) modules. SJTU
2020/10/09 2pm-3pm 白占强 Gelfand-Kirillov dimensions and associated varieties of highest weight modules II See above SJTU
2020/10/09 3:30pm-4:30pm 余世霖 Geometric quantization I The speaker will introduce the notion of Poisson algebra and deformation quantization SJTU
2020/10/16 2:00pm-3:00pm 腾讯会议 ID：864 4848 4933 会议密码：1122 余世霖 Geometric quantization II The speaker will continue his talk last week on the notion of Poisson algebra and deformation quantization. Then he will discuss some results on the quantization of a nilpotent coadjoint orbit of a real reductive Lie group. SJTU
2020/10/16 3:30pm-4:30pm see above 马家骏 Associated character formula in Howe correspondence I I will discuss the joint works with Loke and Barbasch-Sun-Zhu on the formula of the associated character of a local theta lifting (Howe correspondence). Furthermore, I will explain its applications in the construction of unipotent representations and geometric quantization. XMU
2020/10/23 2:00pm-3:00pm see above 马家骏 Associated character formula in Howe correspondence II see above see above
2020/10/23 3:30pm-4:30pm see above Daniel Wong On NON-unitary (g,K)-modules for complex simple Lie groups I We discuss several techniques detecting non-unitarity of representations of complex Lie groups G, such as bottom layer K-types, Dirac inequality and deformation of parameters. These techniques are essential in determining the unitary spectrum of G. We will also briefly mention where the difficulties arise as one applies the same techniques for general real reductive groups. SJTU
2020/10/30 2:00pm-3:00pm Zoom: 61208845721 pass:130094 Daniel Wong On NON-unitary (g,K)-modules for complex simple Lie groups II See above SJTU
2020/10/30 3:30pm-4:30pm Zoom: 61208845721 pass:130094 Li Ning On certain invariants for constituents of degenerate principal series of Sp(2n,R) In this talk, I will describe associated cycles and wave front cycles for irreducible constituents of degenerate principal series of Sp(2n,R), and their relationship with the space of generalized Whittaker models of these representations. This can be achieved by a careful study of Loke-Ma and Gomez-Zhu’s work. SJTU

2019-秋季 线性代数 MA270

课程信息

  • 时间： 星期一 第3节–第4节（10:00 AM – 11:40AM）、星期四(双周)) 第1节–第2节（8:00AM – 9:40AM）
  • 地点： 下院114 (1-16周)
  • 课本： 上海交通大学数学系，线性代数（第三版），科学出版社，2014
  • MOOC(慕课)地址

分数比例

平时：20%，大作业: 10% 期末：70%

大作业

就线性代数中有意思的定理,例题或相关应用写一份学习报告. 报告长度控制在2面A4纸以内.
12月22日23:59前请将大作业发至邮箱: hoxide@sjtu.edu.cn
邮件标题格式: 2019线性代数大作业-xxxxxxxxx-姓名 (xxxxxxxxx为学号)

答疑时间

课件(ppt)

作业:

  • 作业1, 9月23日交: p41 习题一: 1.2, 1.3, 1.5, 3, 4, 7
  • 作业2, 9月30日交: 习题一: 8.1, 11.1, 12.1, 12.4, 12.5, 12.6, 13.1, 13.3, 19.2, 20.4
  • 作业3, 10月14日交: 习题一: 14.1, 14.3, 14.5, 15, 16, 17
  • 作业4, 10月21日交: 习题二: 6, 7.1, 7.3, 8, 9, 10, 13, 15, 17, 27, 32, 33
  • 作业5, 10月28日交: 习题二: 21.2, 21.7,22.1,22.3, 22.4, 26, 28
  • 作业6, 11月11日交: 习题二: 47, 48, 49, 51.1, 51.3, 51.5, 52, 53, 54 习题三: 1, 3, 4, 6.1, 6.2, 7.1, 8 思考题(不用交) 9
  • 作业7, 11月18日交: 习题三: 17, 19.2, 20.2, 22, 23, 24.1,24.3, 24.5, 25, 26, 27.1, 27.2, 28.2, 33, 35
  • 作业8, 12月02日交: 习题四: 3.1, 3.2, 3.3, 4.1, 4.3, 4.5, 6.1, 6.2, 6.3, 7, 9, 12, 13.2, 17
  • 作业9, 12月09日交: 习题四: 18, 19, 22, 23.1, 24 思考题: 25
  • 作业10, 12月16日交: 习题五: 1.3, 1.4, 1.6, 2, 6, 7, 11, 12, 17.2, 20, 22

2019 春季 代数拓扑

课程信息

习题

  • 3月13日交，选做2题: Chapter 0: 4, 11, 13, 15, 23, 26
  • 3月27日交，选做2题:
    Section 1.1: 14, 15, 16 (f);
    Section 1.2: 6, 7, 8, 14, 19,20, 21;
    Section 1.3: 8, 9, 18, 26, 28, 32

    • 4月17日交, 选做3题:
      Section 2.1: 4, 9, 28, 29, 31
    • 5月29日交, 选做3题:
      Section 3.1: 5, 7, 8, 9
      Section 3.2: 2, 9, 10, 11, 15

期中题目

以下三组题中选做一组, 5月8日交

Section 1.2: 20, Section 2.1: 20, 21, Section 2.2: 26
Section 1.2: 21, Section 2.1: 17 (a), Section 2.2: 36
Section 1.3: 28, Section 2.1: 17 (b), Section 2.2: 40, 42