chore: Update Lean and dependencies on 2026/02/17

[SnO2WMaN]

No description provided.

[SnO2WMaN]

@iehality 　ComputabilityとArithmetic辺りに起因する修正を別ブランチ切ってやってもらえると助かる．

[iehality]

v4.29.0-rcn には不安定な箇所がいくつかある（いくつかのエラーはこのために生じている）ので安定版に到達するまでアップデートは待ったほうが良いと思う．

However: unlike most months we do not yet advise downstream projects to move to v4.29.0-rc1, which is more of a :construction_zone: release candidate :construction_zone: than usual, and we will certainly be making further release candidates in this series before reaching a stable version.

• https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/releases.20of.20new.20Lean.20versions/near/574617729

[AlexeyMilovanov]

Hello! I am a theoretical computer scientist (https://alexeymilovanov.github.io/) and I recently created a repository formalizing Kolmogorov complexity in Lean 4: https://github.com/AlexeyMilovanov/kolmogorov-complexity-lean

I have formalized Chaitin's Incompleteness Theorem for a general axiomatic system, and I would like to show that Peano Arithmetic (PA) is a special case. I would love to use your excellent repository to show this, but unfortunately, I cannot import Foundation directly. My project uses a recent Lean 4 / Mathlib toolchain, while your repository is currently pinned to an older version.

I noticed this Draft PR (#758) where you started updating the toolchain but paused waiting for a stable Lean release. Since a stable version is available now, do you plan to resume this update?

If so, I can try to help with the migration and fix the remaining compilation errors (I saw the mention of broken proofs in Arithmetic and Computability).

Let me know what you think!

[SnO2WMaN]

@AlexeyMilovanov

Hello! I am a theoretical computer scientist (https://alexeymilovanov.github.io/) and I recently created a repository formalizing Kolmogorov complexity in Lean 4: https://github.com/AlexeyMilovanov/kolmogorov-complexity-lean

I have formalized Chaitin's Incompleteness Theorem for a general axiomatic system, and I would like to show that Peano Arithmetic (PA) is a special case. I would love to use your excellent repository to show this, but unfortunately, I cannot import Foundation directly. My project uses a recent Lean 4 / Mathlib toolchain, while your repository is currently pinned to an older version.

I noticed this Draft PR (#758) where you started updating the toolchain but paused waiting for a stable Lean release. Since a stable version is available now, do you plan to resume this update?

If so, I can try to help with the migration and fix the remaining compilation errors (I saw the mention of broken proofs in Arithmetic and Computability).

Let me know what you think!

Thank you for reaching out. On our think, we're planning to work on PR once Lean 4.29 is officially reelased, since we have concern about instability of rc version.
That said, if you're hurry, we would like to involve this PR.

On the other hands, I personally find your Kolmogorov complexity formalization project quite interesting. I've been wanting to mechanize Kritchman and Raz's "The Surprise Examination Paradox and the Second Incompleteness Theorem": in case you're not familiar with it, the rough idea is that by formalizing the argument about Kolmogorov complexity within PA, and mechanizing the phenomena like the surprising examination paradox. one can derive Gödel's 2nd incompleteness and related results.
If you're open to it, I'd like to offer help from our side as well, Refer to https://github.com/orgs/FormalizedFormalLogic/discussions/695

[iehality]

Since the stable version v29.0 has already been released, I think we can get started on this right away.

[AlexeyMilovanov]

@SnO2WMaN @iehality
Thank you for pointing me to the Kritchman and Raz paper! I actually learned about it from your comment. I found the approach so elegant that I went ahead and formalized their abstract proof of the Second Incompleteness Theorem in my repository today.

To cleanly separate the information-theoretic paradox from the first-order logic boilerplate, I created an abstract PeanoLikeSystem interface. Once Foundation is updated, we can instantiate it for PA. To make the integration work, the interface only requires the following from the formal system:

1. HBL conditions: A proof inside the system that $Con \to \neg \exists x, Pr(K(x) > L)$ (Equation 1 in the KR paper).
2. $\Sigma_1$-completeness: A proof inside the system for the elimination step: if $m = i$, the system can compute all simple strings to find the remaining complex one (Equation 2 in the KR paper).
3. Internal Arithmetic: A proof inside the system of the base Pigeonhole Principle ($m \ge 1$) and the basic dichotomy step ($m \ge i \to m \neq i \to m \ge i+1$).
4. Semantic Soundness: A standard soundness assumption. This allows us to avoid proving the upper counting bound ($m \le 2^{L+1}+1$) internally; instead, Lean's omega derives the final KR contradiction automatically on the meta-level.

[SnO2WMaN]

@AlexeyMilovanov

This looks great! (I am reading through your code right now.)
Since commenting here on the update issue would confusing the discussion, let's continue in a separate issue.
Please use the following branch for further discussion: https://github.com/orgs/FormalizedFormalLogic/discussions/817 thanks

[SnO2WMaN]

@iehality

とりあえず現状のModalとPropositional周りは終わったのでよろしく頼む．また問題が起きたら連絡してほしい．

[iehality]

メモ：以前生じた問題は v4.29.0 でも改善していない．

• https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Rewriting.2Fsimplification.20issue.20in.20v4.2E29.2E0-rc2

[iehality]

修正完了しました． @SnO2WMaN

[SnO2WMaN]

@AlexeyMilovanov FYI we've done update to v4.29 so you can continue thanks.