Document (#40260)

Author

Hartnett, K.

Title

Werden Computer das Wesen der Mathematik verändern?

Source

Spektrum der Wissenschaft. 2016, H.12, S.60-65

Year

2016

Series

Mathematik

Abstract

Einer der größten Mathematiker der Gegenwart findet in einer eigenen Arbeit einen Fehler - und stürzt sich in ein Projekt mit dem Ziel, das Beweisen gänzlich dem Computer anzuvertrauen. Dazu muss er nichts weniger als die Grundlagen der Mathematik neu fassen. Bericht über das Programm von Vladimir Voevodsky und sein Programm Coq, das über eine Formalisierung auf Basis der Typentheorie das rechnergestützte Überprüfen von mathematischen Aussagen und Beweisen ermöglichen soll.

Field

Mathematik

Similar documents (content)

1. Heintz, B.: ¬Die Innenwelt der Mathematik : Zur Kultur und Praxis einer beweisenden Disziplin (2000) 0.14

   0.14427567 = sum of:
     0.14427567 = product of:
       0.6011486 = sum of:
         0.018400012 = weight(abstract_txt:einer in 736) [ClassicSimilarity], result of:
           0.018400012 = score(doc=736,freq=1.0), product of:
             0.0866332 = queryWeight, product of:
               1.2536902 = boost
               3.8837 = idf(docFreq=2472, maxDocs=44218)
               0.01779297 = queryNorm
             0.21238984 = fieldWeight in 736, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               3.8837 = idf(docFreq=2472, maxDocs=44218)
               0.0546875 = fieldNorm(doc=736)
         0.10478985 = weight(abstract_txt:mathematischen in 736) [ClassicSimilarity], result of:
           0.10478985 = score(doc=736,freq=2.0), product of:
             0.17404643 = queryWeight, product of:
               1.2565091 = boost
               7.7848644 = idf(docFreq=49, maxDocs=44218)
               0.01779297 = queryNorm
             0.60207987 = fieldWeight in 736, product of:
               1.4142135 = tf(freq=2.0), with freq of:
                 2.0 = termFreq=2.0
               7.7848644 = idf(docFreq=49, maxDocs=44218)
               0.0546875 = fieldNorm(doc=736)
         0.15175705 = weight(abstract_txt:mathematiker in 736) [ClassicSimilarity], result of:
           0.15175705 = score(doc=736,freq=4.0), product of:
             0.17682414 = queryWeight, product of:
               1.2664961 = boost
               7.84674 = idf(docFreq=46, maxDocs=44218)
               0.01779297 = queryNorm
             0.85823715 = fieldWeight in 736, product of:
               2.0 = tf(freq=4.0), with freq of:
                 4.0 = termFreq=4.0
               7.84674 = idf(docFreq=46, maxDocs=44218)
               0.0546875 = fieldNorm(doc=736)
         0.019572768 = weight(abstract_txt:über in 736) [ClassicSimilarity], result of:
           0.019572768 = score(doc=736,freq=1.0), product of:
             0.09027631 = queryWeight, product of:
               1.279779 = boost
               3.964518 = idf(docFreq=2280, maxDocs=44218)
               0.01779297 = queryNorm
             0.21680959 = fieldWeight in 736, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               3.964518 = idf(docFreq=2280, maxDocs=44218)
               0.0546875 = fieldNorm(doc=736)
         0.025286723 = weight(abstract_txt:computer in 736) [ClassicSimilarity], result of:
           0.025286723 = score(doc=736,freq=1.0), product of:
             0.107086316 = queryWeight, product of:
               1.3938469 = boost
               4.317879 = idf(docFreq=1601, maxDocs=44218)
               0.01779297 = queryNorm
             0.23613402 = fieldWeight in 736, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               4.317879 = idf(docFreq=1601, maxDocs=44218)
               0.0546875 = fieldNorm(doc=736)
         0.2813422 = weight(abstract_txt:mathematik in 736) [ClassicSimilarity], result of:
           0.2813422 = score(doc=736,freq=7.0), product of:
             0.27899486 = queryWeight, product of:
               2.2498116 = boost
               6.9694996 = idf(docFreq=112, maxDocs=44218)
               0.01779297 = queryNorm
             1.0084136 = fieldWeight in 736, product of:
               2.6457512 = tf(freq=7.0), with freq of:
                 7.0 = termFreq=7.0
               6.9694996 = idf(docFreq=112, maxDocs=44218)
               0.0546875 = fieldNorm(doc=736)
       0.24 = coord(6/25)
   

2. Stammbach, U.: ¬"Die Mathematik ist eine gar herrliche Wissenschaft" (2005) 0.14

   0.13957699 = sum of:
     0.13957699 = product of:
       0.49848926 = sum of:
         0.044244442 = weight(abstract_txt:nichts in 5095) [ClassicSimilarity], result of:
           0.044244442 = score(doc=5095,freq=1.0), product of:
             0.13677266 = queryWeight, product of:
               1.1138654 = boost
               6.901097 = idf(docFreq=120, maxDocs=44218)
               0.01779297 = queryNorm
             0.32348892 = fieldWeight in 5095, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               6.901097 = idf(docFreq=120, maxDocs=44218)
               0.046875 = fieldNorm(doc=5095)
         0.050656453 = weight(abstract_txt:aussagen in 5095) [ClassicSimilarity], result of:
           0.050656453 = score(doc=5095,freq=1.0), product of:
             0.14968674 = queryWeight, product of:
               1.1652651 = boost
               7.2195506 = idf(docFreq=87, maxDocs=44218)
               0.01779297 = queryNorm
             0.33841643 = fieldWeight in 5095, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               7.2195506 = idf(docFreq=87, maxDocs=44218)
               0.046875 = fieldNorm(doc=5095)
         0.01577144 = weight(abstract_txt:einer in 5095) [ClassicSimilarity], result of:
           0.01577144 = score(doc=5095,freq=1.0), product of:
             0.0866332 = queryWeight, product of:
               1.2536902 = boost
               3.8837 = idf(docFreq=2472, maxDocs=44218)
               0.01779297 = queryNorm
             0.18204844 = fieldWeight in 5095, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               3.8837 = idf(docFreq=2472, maxDocs=44218)
               0.046875 = fieldNorm(doc=5095)
         0.08981987 = weight(abstract_txt:mathematischen in 5095) [ClassicSimilarity], result of:
           0.08981987 = score(doc=5095,freq=2.0), product of:
             0.17404643 = queryWeight, product of:
               1.2565091 = boost
               7.7848644 = idf(docFreq=49, maxDocs=44218)
               0.01779297 = queryNorm
             0.51606846 = fieldWeight in 5095, product of:
               1.4142135 = tf(freq=2.0), with freq of:
                 2.0 = termFreq=2.0
               7.7848644 = idf(docFreq=49, maxDocs=44218)
               0.046875 = fieldNorm(doc=5095)
         0.09197866 = weight(abstract_txt:mathematiker in 5095) [ClassicSimilarity], result of:
           0.09197866 = score(doc=5095,freq=2.0), product of:
             0.17682414 = queryWeight, product of:
               1.2664961 = boost
               7.84674 = idf(docFreq=46, maxDocs=44218)
               0.01779297 = queryNorm
             0.5201703 = fieldWeight in 5095, product of:
               1.4142135 = tf(freq=2.0), with freq of:
                 2.0 = termFreq=2.0
               7.84674 = idf(docFreq=46, maxDocs=44218)
               0.046875 = fieldNorm(doc=5095)
         0.02372578 = weight(abstract_txt:über in 5095) [ClassicSimilarity], result of:
           0.02372578 = score(doc=5095,freq=2.0), product of:
             0.09027631 = queryWeight, product of:
               1.279779 = boost
               3.964518 = idf(docFreq=2280, maxDocs=44218)
               0.01779297 = queryNorm
             0.2628129 = fieldWeight in 5095, product of:
               1.4142135 = tf(freq=2.0), with freq of:
                 2.0 = termFreq=2.0
               3.964518 = idf(docFreq=2280, maxDocs=44218)
               0.046875 = fieldNorm(doc=5095)
         0.18229261 = weight(abstract_txt:mathematik in 5095) [ClassicSimilarity], result of:
           0.18229261 = score(doc=5095,freq=4.0), product of:
             0.27899486 = queryWeight, product of:
               2.2498116 = boost
               6.9694996 = idf(docFreq=112, maxDocs=44218)
               0.01779297 = queryNorm
             0.6533906 = fieldWeight in 5095, product of:
               2.0 = tf(freq=4.0), with freq of:
                 4.0 = termFreq=4.0
               6.9694996 = idf(docFreq=112, maxDocs=44218)
               0.046875 = fieldNorm(doc=5095)
       0.28 = coord(7/25)
   

3. Behrends, E.: Fünf Minuten Mathematik : 100 Beiträge der Mathematik-Kolumne der Zeitung DIE WELT (2006) 0.14

   0.1371833 = sum of:
     0.1371833 = product of:
       0.6859164 = sum of:
         0.058502454 = weight(abstract_txt:findet in 471) [ClassicSimilarity], result of:
           0.058502454 = score(doc=471,freq=1.0), product of:
             0.117213346 = queryWeight, product of:
               1.0311494 = boost
               6.3886194 = idf(docFreq=201, maxDocs=44218)
               0.01779297 = queryNorm
             0.49911088 = fieldWeight in 471, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               6.3886194 = idf(docFreq=201, maxDocs=44218)
               0.078125 = fieldNorm(doc=471)
         0.026285728 = weight(abstract_txt:einer in 471) [ClassicSimilarity], result of:
           0.026285728 = score(doc=471,freq=1.0), product of:
             0.0866332 = queryWeight, product of:
               1.2536902 = boost
               3.8837 = idf(docFreq=2472, maxDocs=44218)
               0.01779297 = queryNorm
             0.30341405 = fieldWeight in 471, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               3.8837 = idf(docFreq=2472, maxDocs=44218)
               0.078125 = fieldNorm(doc=471)
         0.105853744 = weight(abstract_txt:mathematischen in 471) [ClassicSimilarity], result of:
           0.105853744 = score(doc=471,freq=1.0), product of:
             0.17404643 = queryWeight, product of:
               1.2565091 = boost
               7.7848644 = idf(docFreq=49, maxDocs=44218)
               0.01779297 = queryNorm
             0.60819256 = fieldWeight in 471, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               7.7848644 = idf(docFreq=49, maxDocs=44218)
               0.078125 = fieldNorm(doc=471)
         0.039542962 = weight(abstract_txt:über in 471) [ClassicSimilarity], result of:
           0.039542962 = score(doc=471,freq=2.0), product of:
             0.09027631 = queryWeight, product of:
               1.279779 = boost
               3.964518 = idf(docFreq=2280, maxDocs=44218)
               0.01779297 = queryNorm
             0.43802148 = fieldWeight in 471, product of:
               1.4142135 = tf(freq=2.0), with freq of:
                 2.0 = termFreq=2.0
               3.964518 = idf(docFreq=2280, maxDocs=44218)
               0.078125 = fieldNorm(doc=471)
         0.45573154 = weight(abstract_txt:mathematik in 471) [ClassicSimilarity], result of:
           0.45573154 = score(doc=471,freq=9.0), product of:
             0.27899486 = queryWeight, product of:
               2.2498116 = boost
               6.9694996 = idf(docFreq=112, maxDocs=44218)
               0.01779297 = queryNorm
             1.6334765 = fieldWeight in 471, product of:
               3.0 = tf(freq=9.0), with freq of:
                 9.0 = termFreq=9.0
               6.9694996 = idf(docFreq=112, maxDocs=44218)
               0.078125 = fieldNorm(doc=471)
       0.2 = coord(5/25)
   

4. Nohr, H.: Rechnergestützte Gruppenarbeit : Computer-Supported Cooperative Work (CSCW) (2004) 0.14

   0.13641846 = sum of:
     0.13641846 = product of:
       1.1368206 = sum of:
         0.054111663 = weight(abstract_txt:grundlagen in 2940) [ClassicSimilarity], result of:
           0.054111663 = score(doc=2940,freq=1.0), product of:
             0.1112726 = queryWeight, product of:
               1.0046787 = boost
               6.2246165 = idf(docFreq=237, maxDocs=44218)
               0.01779297 = queryNorm
             0.48629817 = fieldWeight in 2940, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               6.2246165 = idf(docFreq=237, maxDocs=44218)
               0.078125 = fieldNorm(doc=2940)
         0.036123887 = weight(abstract_txt:computer in 2940) [ClassicSimilarity], result of:
           0.036123887 = score(doc=2940,freq=1.0), product of:
             0.107086316 = queryWeight, product of:
               1.3938469 = boost
               4.317879 = idf(docFreq=1601, maxDocs=44218)
               0.01779297 = queryNorm
             0.3373343 = fieldWeight in 2940, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               4.317879 = idf(docFreq=1601, maxDocs=44218)
               0.078125 = fieldNorm(doc=2940)
         1.046585 = weight(title_txt:rechnergestützte in 2940) [ClassicSimilarity], result of:
           1.046585 = score(doc=2940,freq=1.0), product of:
             0.28176248 = queryWeight, product of:
               1.5987283 = boost
               9.905128 = idf(docFreq=5, maxDocs=44218)
               0.01779297 = queryNorm
             3.7144227 = fieldWeight in 2940, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               9.905128 = idf(docFreq=5, maxDocs=44218)
               0.375 = fieldNorm(doc=2940)
       0.12 = coord(3/25)
   

5. Reiss, K.; Ufer, S.: Was macht mathematisches Arbeiten aus? : Empirische Ergebnisse zum Argumentieren, Begründen und Beweisen (2009) 0.13

   0.13207334 = sum of:
     0.13207334 = product of:
       0.8254584 = sum of:
         0.08442742 = weight(abstract_txt:aussagen in 1209) [ClassicSimilarity], result of:
           0.08442742 = score(doc=1209,freq=1.0), product of:
             0.14968674 = queryWeight, product of:
               1.1652651 = boost
               7.2195506 = idf(docFreq=87, maxDocs=44218)
               0.01779297 = queryNorm
             0.56402737 = fieldWeight in 1209, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               7.2195506 = idf(docFreq=87, maxDocs=44218)
               0.078125 = fieldNorm(doc=1209)
         0.105853744 = weight(abstract_txt:mathematischen in 1209) [ClassicSimilarity], result of:
           0.105853744 = score(doc=1209,freq=1.0), product of:
             0.17404643 = queryWeight, product of:
               1.2565091 = boost
               7.7848644 = idf(docFreq=49, maxDocs=44218)
               0.01779297 = queryNorm
             0.60819256 = fieldWeight in 1209, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               7.7848644 = idf(docFreq=49, maxDocs=44218)
               0.078125 = fieldNorm(doc=1209)
         0.1519105 = weight(abstract_txt:mathematik in 1209) [ClassicSimilarity], result of:
           0.1519105 = score(doc=1209,freq=1.0), product of:
             0.27899486 = queryWeight, product of:
               2.2498116 = boost
               6.9694996 = idf(docFreq=112, maxDocs=44218)
               0.01779297 = queryNorm
             0.5444921 = fieldWeight in 1209, product of:
               1.0 = tf(freq=1.0), with freq of:
                 1.0 = termFreq=1.0
               6.9694996 = idf(docFreq=112, maxDocs=44218)
               0.078125 = fieldNorm(doc=1209)
         0.48326677 = weight(abstract_txt:beweisen in 1209) [ClassicSimilarity], result of:
           0.48326677 = score(doc=1209,freq=2.0), product of:
             0.4789817 = queryWeight, product of:
               2.9478645 = boost
               9.131938 = idf(docFreq=12, maxDocs=44218)
               0.01779297 = queryNorm
             1.0089462 = fieldWeight in 1209, product of:
               1.4142135 = tf(freq=2.0), with freq of:
                 2.0 = termFreq=2.0
               9.131938 = idf(docFreq=12, maxDocs=44218)
               0.078125 = fieldNorm(doc=1209)
       0.16 = coord(4/25)