Discussion: Upgrading to Lean v4.29.1 / current Mathlib#3
Draft
ChihChengLiang wants to merge 10 commits intoTimeroot:mainfrom
Draft
Discussion: Upgrading to Lean v4.29.1 / current Mathlib#3ChihChengLiang wants to merge 10 commits intoTimeroot:mainfrom
ChihChengLiang wants to merge 10 commits intoTimeroot:mainfrom
Conversation
- Update lean-toolchain to v4.30.0-rc1 - Run lake update to refresh all dependencies - Fix removed/moved Mathlib modules: - Mathlib.Data.Sign → Mathlib.Data.Sign.Basic - Mathlib.Data.Real.GoldenRatio → Mathlib.NumberTheory.Real.GoldenRatio - Mathlib.Data.Real.Pi.Bounds → Mathlib.Analysis.Real.Pi.Bounds - Mathlib.Data.Complex.Exponential → Mathlib.Analysis.Complex.Exponential - Fix removed typeclasses in aux_lemmas.lean: - LinearOrderedAddCommGroup → AddCommGroup + LinearOrder + IsOrderedAddMonoid - LinearOrderedField → Field + LinearOrder + IsStrictOrderedRing Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
ChihChengLiang
commented
Apr 22, 2026
| let signed := x.dropTilSigned hnz | ||
| let hnz' := val_dropTilSigned hnz ▸ hnz | ||
| -- x.val⁻¹ use `Real.instInv` here, which is noncomputable. | ||
| mk (x := x.val⁻¹) |
Author
There was a problem hiding this comment.
x.val⁻¹ here use the Real.instInv
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Discussion: Upgrading to Lean v4.29.1 / current Mathlib
Not for merging — opening this as a discussion to share findings and get feedback.
Background
Hi Timeroot, thanks for building this great project! I was learning Lean, encountered problem computing real numbers, and then found this project.
I tried upgrading ComputableReal from Lean v4.17.0-rc1 to v4.29.1 with a compatible Mathlib version. This PR captures my attempt and the problem I ran into.
The Core Problem
Real.instInvisnoncomputablein Lean v4.29.1. Since ComputableReal's whole approach depends on being able to compute with real numbers, this creates a cascading issue — the noncomputability propagates to nearly every definition and instance that touches it, which largely defeats the purpose of the project.What I tried
Real.instInvatsafe_invWhere I'm stuck
The noncomputability of
Real.instInvseems fundamental rather than incidental. I'm not sure whether the right path is:Real.instInvQuestions for the maintainer
Real.instInv?Happy to keep iterating on this if it's useful — just wanted to surface the findings first before going further.