李嘉图 Jiatu Li

Basic information

I am a third-year undergraduate student in the Yao Class, Institute for Interdisciplinary Information Science (IIIS), Tsinghua University. My research interest is about circuit complexity, proof complexity, and cryptography. Currently I am thinking about problems about bounded arithmetic (fragments of Peano that captures the complexity of proofs).

I am also interested in writing formal (i.e. computer verified) mathematical proofs in Coq and Lean. Although it seems to be incredible nowadays, I believe that proof assistants will eventually be able to help mathematicians in their research (if mathematicians are not completely replaced by something like GPT-256).

How to contact me?

• Email 1: lijt19@mails.tsinghua.edu.cn
• Email 2: ljt714285@gmail.com
• Github: http://github.com/ljt12138/

If you have any questions or comments about my papers, essays, and any other projects, please feel free to contact me. I will be more than happy to hear from anyone interested in my works.

My works

Research papers

• $3.1n−o(n)$ Circuit Lower Bounds for Explicit Functions.
  • A joint work with Tianqi Yang.
  • To appear in the 54th ACM Symposium on Theory of Computing (STOC 2022).
  • Summary. We improve the $(3 + 1/86)n + o(n)$ unconditional circuit lower bound (for explicit function in $\mathsf{P}$ to $3.1n + o(n)$ with a more clever choice of complexity measure and a more careful case analysis.
• The Exact Complexity of Pseudorandom Functions and the Black-Box Natural Proof Barrier for Bootstrapping Results in Computational Complexity.
  • A joint work with Zhiyuan Fan and Tianqi Yang.
  • To appear in the 54th ACM Symposium on Theory of Computing (STOC 2022).
  • Summary. We give tight bounds to compute PRFs in general $\mathsf{B}_2$ circuit (in size), $\mathsf{NC}_1$ circuits (in size and depth) and $\mathsf{TC}_0$ circuits (in wire). Inspired by the natural proof barrier and our results, we demonstrate a barrier for bootstrapping results (e.g. hardness magnification) in complexity theory.

Other projects

• Formalization of PAL·S5 in Proof Assistant.
  • Technical Report: https://arxiv.org/abs/2012.09388.
  • Talk in LIRa seminar: https://projects.illc.uva.nl/lgc/seminar/2021/03/lira-session-jiatu-li/
  • Summary. We formalize public announcement logic (a special kind of dynamic epistemic logic) in Lean theorem prover as an experiment to apply formal tools in logic research. We present formal proof of its soundness, completeness and reduction (i.e. elimination of dynamic modalities) theorem.
• Formalization of a theorem in a competitive programming problem.
  • Github: https://github.com/ljt12138/Proof-of-Surreal
• Cutepiler: A Compiler for a C-like Language.
  • Github: https://github.com/Cutepiler/Cutepiler-Sysy2020
  • In National Student Computer System Capability Challenge (Compiler track).
  • A joint work with Runda Liu, Zhidong Wang and Mengdi Wu.
• Hyper OS: An Operating System Simulator in C++.
  • Github: https://github.com/tqyaaaaang/Hyper-OS
  • A joint work with Tianqi Yang.
  • Summary. An operating system simulator for teaching and research use in C++. It contains basic virtual hardwares (such as CPU, APIC, MMU, etc) and a tiny kernel (including process scheduling and paging).

Notes, talks, and essays

• A Quick Introduction to Mathematical Logic.
  • Note: https://ljt12138.github.io/2020/05/05/logic-note/
  • Summary. A note on classical results about propositional logic, first-order logic, proof system and (basic) model theory. It covers completeness theorem of first-order logic, compactness theorem and G¨odel’s incompleteness theorem.
• The Application of Non-Programming Problems in Competitive Programming Training (in Chinese).
  • Essay: https://ljt12138.github.io/2020/01/09/wc-final/

Interesting facts about me

• My name, Li Jiatu, is the same as the Chinese translation of Ricardo. My parents choose the name when they are reading The Capital of Karl Marx, in which the name David Ricardo occurs constantly.

Abstract: In this work, we provide a quick introduction to the classical results about propositional logic, first-order logic, proof system and (basic) model theory, for the readers who are familiar with (informal) set theory and logic. We will cover the completeness theorem of first-order logic, the compactness theorem, Tarski’s undefinability theorem and Gödel’s incompleteness theorem, and is suitable for mathematics or computer science students who are interested in mathematical logic.

概述：本文将介绍如何实现一个非常简单的命题逻辑定理证明器。这个定理证明器用 Haskell 编写，以交互式的方式进行使用，输出 Hilbert Style System 下原命题的一个证明。用这个小工具，我们可以生成许多难以直接证明的定理（如析取、合取的结合律）的证明。

简单类型 λ 演算

简单类型 λ 演算是一种非常简单的类型系统。在本文中，我们将从简单类型 λ 演算的基本性质出发，介绍四个不那么平凡的结果：

• 强正则定理：简单类型 λ 演算中，不存在以有类型的项开始的无限长的 β 规约序列；
• 类型推导算法：对于 Curry 风格（变量不注明类型）的 λ 演算，存在高效的算法求出 λ 项的“主类型”；
• 组合子逻辑：一个仅用 2 个组合子和组合子应用形成的演算系统，不需要任何变量；
• Curry-Howard 同构：简单类型 λ 演算与直觉主义命题逻辑的自然演绎系统对应，简单类型组合子逻辑与直觉主义希尔伯特公理系统对应。

摘要：程序设计题目是目前信息学竞赛主要的教学、训练方式。本文从程序设计题目在信息学竞赛教学中的不足出发，通过分析传统的教学模式，探讨了非程序设计题目在信息学竞赛教学中的应用价值。此外，通过引入阶段性模型提出了面向教学目标的非程序设计题目设计方法，总结出一些有效的非程序设计题目形式。本文认为，非程序设计题目作为传统程序设计题目训练的补充，可以在缺乏教师指导的情况下提升整体教学效果，是一种值得推广的教学设计方法。

关键词：信息学竞赛教育，教学方法，教学研究，非程序设计题目

概述

k-sorter 问题指如何利用“给 k 个元素排序”这一基本操作，构造高效的排序算法。由于一个 k-sorter 可以由 $k\log k$ 次比较操作构造，而比较排序的时间复杂度下界是 $n\log n$，因此 k-sorter 问题的排序器使用次数下界（下称比较下界）为 $n\log n/k\log k$。我对这个问题的了解来自于清华大学邓俊辉老师的《数据结构》课程中的一道编程练习题（题目对应 $k=3$ 的情景），并将一个简单的做法（$n\log n/k$ 次比较的算法）出做了集训队作业题目¹。近期我对此问题又做了一些调查和探索，结论如下：

• 存在若干种比较次数在 $O(n\log n/k)$ 的确定性排序算法，包括两个比较简单的基于归并的算法；
• 存在期望 $O(n\log n/k\log k)$ 次比较的随机算法，这一算法思路简单，但分析稍加繁琐；
• 存在 $(n\log n/k\log k)$ 次比较的确定性算法，这一算法来自².

$k$ 祖先问题

$k$ 祖先问题（Level Ancestor Problem）是静态树的重要问题之一。给定一棵树和若干个询问 $(u, k)$，要求结点 $u$ 的第 $k​$ 个祖先结点。

离线情景下的 $k$ 祖先问题存在一个简单的 $O(n+q)$ 的算法：在 dfs 的过程中维护一个记录祖先的栈，然后在每个结点处回答和这个结点有关的所有询问；在线情景下有基于倍增的 $O(n\log n)-O(\log n)$ 算法，基于长链剖分的 $O(n)-O(\log n)$ 算法和 $O(n\log n) - O(1)$ 算法，以及最终的 $O(n) - O(1)$ 算法。

缓存无关模型

在算法层面考虑储存器层次结构时，我们通常使用的是外部储存模型（External Memory Model）。在这样的模型中，储存器具有两级 $L_1, L_2$，且 $|L_1| = M, |L_2| = \infty$。$L_1$ 被看作 $L_2$ 的缓存，当访问的数据不在 $L_1$ 中时，我们将数据从 $L_2$ 中调入 $L_1$，并花费 $T$ 的传输时间。

Stage0

某天深夜水群的时候给小朋友普及 Tarjan 算法求 LCA 的时间复杂度，被老鸽们指正应当是 $O(n+q)$ 而非$O((n+q)\alpha(n))$。最近阅读了一下 wiki 上指出的论文 ¹ 学习了一下。

先放结论：RMQ 问题和 LCA 问题的最优复杂度都是 $O(n)-O(1)$ 的，线性复杂度的 Tarjan 需要做一些操作。

题目

Info

数学题面是英文，物理题面是中文。数学可以用中文或英文做答，物理用中文做答。

数学题是六道组合，感觉相对 OI 友好。