Jove
Visualize
Contact Us

Related Experiment Videos

The challenge of computer mathematics.

Henk Barendregt1, Freek Wiedijk

  • 1Radboud University Nijmegen 6500 GL Nijmegen, The Netherlands. henk@cs.ru.nl

Philosophical Transactions. Series A, Mathematical, Physical, and Engineering Sciences
|September 29, 2005
PubMed
Summary

Foundations of mathematics enable computer systems to verify mathematical concepts, algorithms, and proofs. This integration of human input and machine verification, based on Gödel and Turing

Related Concept Videos

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

Cessations of consciousness in meditation: Advancing a scientific understanding of nirodha samāpatti.

Progress in brain research·2023
Same author

The (In)flexible self: Psychopathology, mindfulness, and neuroscience.

International journal of clinical and health psychology : IJCHP·2023
Same author

Metacognitive awareness of covert somatosensory attention corresponds to contralateral alpha power.

NeuroImage·2013
Same author

Mindfulness reduces habitual responding based on implicit knowledge: evidence from artificial grammar learning.

Consciousness and cognition·2013
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Area of Science:

  • Foundations of Mathematics
  • Computer Science
  • Mathematical Logic

Background:

  • Significant advancements in the foundations of mathematics allow for a unified language to express mathematical concepts, algorithms, and proofs.
  • This progress is partly underpinned by foundational results from Gödel and Turing, enabling formalization of mathematical reasoning.
  • Interactive computer systems are emerging that integrate definition, computation, and proof verification.

Purpose of the Study:

  • To explore the integration of mathematical concepts, algorithms, and proofs within a unified formal language.
  • To leverage foundational mathematical results for the development of interactive computer systems for mathematics.
  • To demonstrate the feasibility and applications of 'computer mathematics' systems.

Main Methods:

  • Formulating mathematical concepts, algorithms, and proofs in a single, impeccable language.
  • Developing interactive computer systems where humans define and prove, and machines verify correctness.
  • Utilizing Gödel's and Turing's results to underpin the formalization of mathematical reasoning.

Main Results:

  • All thinkable mathematical concepts, algorithms, and proofs can be formulated in a single, formal language.
  • Interactive computer systems successfully integrate human-led definition, algorithm construction, and proof provision with machine verification.
  • The feasibility of 'computer mathematics' has been demonstrated, with practical applications identified.

Conclusions:

  • The integration of formal language and interactive computer systems represents a significant step in 'computer mathematics'.
  • Current systems demonstrate the feasibility of machine-assisted mathematical reasoning and verification.
  • Future challenges include enhancing system user-friendliness for mathematicians through libraries and tools to foster broader adoption and application.

Related Experiment Videos