Computer-assisted proofs in analysis
From MaRDI portal
Computers have a number of uses in mathematics and mathematical physics. Two which are relatively familiar are heuristic numerical exploration and determining properties of discrete objects (e.g., testing integers for primality). We describe here an example of a less familiar use of computers: the strict verification of estimates on continuously variable quantities (real numbers) for use in the proof of qualitative statements in analysis.
Recommendations
- scientific article; zbMATH DE number 4108029
- scientific article; zbMATH DE number 5899421
- scientific article; zbMATH DE number 1231647
- Computer-Assisted Proofs in Analysis and Programming in Logic: A case Study
- scientific article; zbMATH DE number 67122
- Computer theorem proving in mathematics
- Computer assisted proofs for spectral problems
- Computerized proof techniques for undergraduates
- On computer-assisted proofs in ordinal number theory
- Computer-assisted proofs in PDE: a survey
Cites work
Cited in
(40)- Construction of analytic KAM-surfaces and effective stability bounds
- Construction of invariant tori for the spin-orbit problem in the Mercury-Sun system
- Integrating computer algebra into proof planning
- Invariant curves for area-preserving twist maps far from integrable
- On computer-assisted proofs in ordinal number theory
- Construction of librational invariant tori in the spin-orbit problem
- Automatic differentiation for Fourier series and the radii polynomial approach
- Chaotic motions in the restricted four body problem via Devaney's saddle-focus homoclinic tangle theorem
- Validated numerics for continuation and bifurcation of connecting orbits of maps
- Computer assisted proofs in dynamical systems
- scientific article; zbMATH DE number 1694747 (Why is no real title available?)
- Computer assisted Fourier analysis in sequence spaces of varying regularity
- scientific article; zbMATH DE number 5899421 (Why is no real title available?)
- A numerical approach to the proof of existence of solutions for elliptic problems
- scientific article; zbMATH DE number 4164180 (Why is no real title available?)
- scientific article; zbMATH DE number 3960891 (Why is no real title available?)
- scientific article; zbMATH DE number 4020334 (Why is no real title available?)
- Calculating proofs on a computer in studies of the properties of linear mappings in finite-dimensional spaces
- Rigorous estimates for a computer-assisted KAM theory
- scientific article; zbMATH DE number 4098591 (Why is no real title available?)
- scientific article; zbMATH DE number 4108029 (Why is no real title available?)
- scientific article; zbMATH DE number 67111 (Why is no real title available?)
- scientific article; zbMATH DE number 67116 (Why is no real title available?)
- scientific article; zbMATH DE number 67122 (Why is no real title available?)
- scientific article; zbMATH DE number 2078143 (Why is no real title available?)
- Accurate strategies for small divisor problems
- Polynomial approximation of one parameter families of (un)stable manifolds with rigorous computer assisted error bounds
- scientific article; zbMATH DE number 927286 (Why is no real title available?)
- PERIOD DOUBLING RENORMALIZATION FOR AREA-PRESERVING MAPS AND MILD COMPUTER ASSISTANCE IN CONTRACTION MAPPING PRINCIPLE
- scientific article; zbMATH DE number 1432037 (Why is no real title available?)
- Torus knot choreographies in the \(n\)-body problem
- Computer-Assisted Proofs in Analysis and Programming in Logic: A case Study
- scientific article; zbMATH DE number 7056222 (Why is no real title available?)
- Certified Computer Algebra on Top of an Interactive Theorem Prover
- Existence of the FS-type renormalisation fixed point for unidirectionally-coupled pairs of maps
- Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
- Validated numerical approximation of stable manifolds for parabolic partial differential equations
- Computer assisted proofs for transverse collision and near collision orbits in the restricted three body problem
- Kolmogorov-Arnold-Moser (KAM) theory for finite and infinite dimensional systems
- Analysis of resonances in the spin-orbit problem in celestial mechanics. I: The synchronous resonance
This page was built for publication: Computer-assisted proofs in analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1080247)
