Zulip Chat Archive
Stream: triage
Topic: issue #1038: Implement computable real numbers
Random Issue Bot (Feb 11 2021 at 14:20):
Today I chose issue 1038 for discussion!
Implement computable real numbers
Created by @Yury G. Kudryashov (@urkud) on 2019-05-16
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 18 2021 at 14:19):
Today I chose issue 1038 for discussion!
Implement computable real numbers
Created by @Yury G. Kudryashov (@urkud) on 2019-05-16
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Nov 18 2021 at 15:35):
I think we could wait for Lean 4 to do this, but then it would be cool to do it. I know that several people have asked me about formally verifying bounds for solutions to differential equations etc using interval arithmetic -- is this related?
Random Issue Bot (Jan 28 2022 at 14:16):
Today I chose issue 1038 for discussion!
Implement computable real numbers
Created by @Yury G. Kudryashov (@urkud) on 2019-05-16
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Jan 29 2022 at 09:23):
Probably worth waiting for lean 4 now, but I thought I'd remark that people from outside pure maths sometimes get in touch with me about whether lean can be used in their area and the question often boils down to things like formally verified arithmetic for estimates of reals. The comment on GitHub implying that the correct formalisation depends on the application is a bit scary though
Random Issue Bot (Nov 17 2022 at 14:08):
Today I chose issue 1038 for discussion!
Implement computable real numbers
Created by @Yury G. Kudryashov (@urkud) on 2019-05-16
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 10 2023 at 14:08):
Today I chose issue 1038 for discussion!
Implement computable real numbers
Created by @Yury G. Kudryashov (@urkud) on 2019-05-16
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 21 2023 at 14:08):
Today I chose issue 1038 for discussion!
Implement computable real numbers
Created by @Yury G. Kudryashov (@urkud) on 2019-05-16
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 10 2023 at 14:07):
Today I chose issue 1038 for discussion!
Implement computable real numbers
Created by @Yury G. Kudryashov (@urkud) on 2019-05-16
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC