Document (#40261)

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.14418663 = sum of:
      0.14418663 = product of:
        0.6007776 = sum of:
          0.01838052 = weight(abstract_txt:einer in 1737) [ClassicSimilarity], result of:
            0.01838052 = score(doc=1737,freq=1.0), product of:
              0.086591564 = queryWeight, product of:
                1.2535831 = boost
                3.8814514 = idf(docFreq=2470, maxDocs=44083)
                0.017796243 = queryNorm
              0.21226688 = fieldWeight in 1737, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                3.8814514 = idf(docFreq=2470, maxDocs=44083)
                0.0546875 = fieldNorm(doc=1737)
          0.10473737 = weight(abstract_txt:mathematischen in 1737) [ClassicSimilarity], result of:
            0.10473737 = score(doc=1737,freq=2.0), product of:
              0.1740276 = queryWeight, product of:
                1.2566358 = boost
                7.7818065 = idf(docFreq=49, maxDocs=44083)
                0.017796243 = queryNorm
              0.6018434 = fieldWeight in 1737, product of:
                1.4142135 = tf(freq=2.0), with freq of:
                  2.0 = termFreq=2.0
                7.7818065 = idf(docFreq=49, maxDocs=44083)
                0.0546875 = fieldNorm(doc=1737)
          0.15168244 = weight(abstract_txt:mathematiker in 1737) [ClassicSimilarity], result of:
            0.15168244 = score(doc=1737,freq=4.0), product of:
              0.1768061 = queryWeight, product of:
                1.2666277 = boost
                7.843682 = idf(docFreq=46, maxDocs=44083)
                0.017796243 = queryNorm
              0.8579027 = fieldWeight in 1737, product of:
                2.0 = tf(freq=4.0), with freq of:
                  4.0 = termFreq=4.0
                7.843682 = idf(docFreq=46, maxDocs=44083)
                0.0546875 = fieldNorm(doc=1737)
          0.019553738 = weight(abstract_txt:über in 1737) [ClassicSimilarity], result of:
            0.019553738 = score(doc=1737,freq=1.0), product of:
              0.09023816 = queryWeight, product of:
                1.2797067 = boost
                3.9623375 = idf(docFreq=2278, maxDocs=44083)
                0.017796243 = queryNorm
              0.21669033 = fieldWeight in 1737, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                3.9623375 = idf(docFreq=2278, maxDocs=44083)
                0.0546875 = fieldNorm(doc=1737)
          0.02526111 = weight(abstract_txt:computer in 1737) [ClassicSimilarity], result of:
            0.02526111 = score(doc=1737,freq=1.0), product of:
              0.10703817 = queryWeight, product of:
                1.3937494 = boost
                4.315446 = idf(docFreq=1600, maxDocs=44083)
                0.017796243 = queryNorm
              0.23600096 = fieldWeight in 1737, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                4.315446 = idf(docFreq=1600, maxDocs=44083)
                0.0546875 = fieldNorm(doc=1737)
          0.28116247 = weight(abstract_txt:mathematik in 1737) [ClassicSimilarity], result of:
            0.28116247 = score(doc=1737,freq=7.0), product of:
              0.27893904 = queryWeight, product of:
                2.2499352 = boost
                6.9664416 = idf(docFreq=112, maxDocs=44083)
                0.017796243 = queryNorm
              1.007971 = fieldWeight in 1737, product of:
                2.6457512 = tf(freq=7.0), with freq of:
                  7.0 = termFreq=7.0
                6.9664416 = idf(docFreq=112, maxDocs=44083)
                0.0546875 = fieldNorm(doc=1737)
        0.24 = coord(6/25)
    
  2. Stammbach, U.: ¬"Die Mathematik ist eine gar herrliche Wissenschaft" (2005) 0.14
    0.13955896 = sum of:
      0.13955896 = product of:
        0.49842486 = sum of:
          0.044215597 = weight(abstract_txt:nichts in 96) [ClassicSimilarity], result of:
            0.044215597 = score(doc=96,freq=1.0), product of:
              0.1367441 = queryWeight, product of:
                1.1139216 = boost
                6.898039 = idf(docFreq=120, maxDocs=44083)
                0.017796243 = queryNorm
              0.32334557 = fieldWeight in 96, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                6.898039 = idf(docFreq=120, maxDocs=44083)
                0.046875 = fieldNorm(doc=96)
          0.050867327 = weight(abstract_txt:aussagen in 96) [ClassicSimilarity], result of:
            0.050867327 = score(doc=96,freq=1.0), product of:
              0.15013577 = queryWeight, product of:
                1.1671923 = boost
                7.2279215 = idf(docFreq=86, maxDocs=44083)
                0.017796243 = queryNorm
              0.33880883 = fieldWeight in 96, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                7.2279215 = idf(docFreq=86, maxDocs=44083)
                0.046875 = fieldNorm(doc=96)
          0.015754731 = weight(abstract_txt:einer in 96) [ClassicSimilarity], result of:
            0.015754731 = score(doc=96,freq=1.0), product of:
              0.086591564 = queryWeight, product of:
                1.2535831 = boost
                3.8814514 = idf(docFreq=2470, maxDocs=44083)
                0.017796243 = queryNorm
              0.18194303 = fieldWeight in 96, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                3.8814514 = idf(docFreq=2470, maxDocs=44083)
                0.046875 = fieldNorm(doc=96)
          0.08977489 = weight(abstract_txt:mathematischen in 96) [ClassicSimilarity], result of:
            0.08977489 = score(doc=96,freq=2.0), product of:
              0.1740276 = queryWeight, product of:
                1.2566358 = boost
                7.7818065 = idf(docFreq=49, maxDocs=44083)
                0.017796243 = queryNorm
              0.5158658 = fieldWeight in 96, product of:
                1.4142135 = tf(freq=2.0), with freq of:
                  2.0 = termFreq=2.0
                7.7818065 = idf(docFreq=49, maxDocs=44083)
                0.046875 = fieldNorm(doc=96)
          0.09193344 = weight(abstract_txt:mathematiker in 96) [ClassicSimilarity], result of:
            0.09193344 = score(doc=96,freq=2.0), product of:
              0.1768061 = queryWeight, product of:
                1.2666277 = boost
                7.843682 = idf(docFreq=46, maxDocs=44083)
                0.017796243 = queryNorm
              0.51996756 = fieldWeight in 96, product of:
                1.4142135 = tf(freq=2.0), with freq of:
                  2.0 = termFreq=2.0
                7.843682 = idf(docFreq=46, maxDocs=44083)
                0.046875 = fieldNorm(doc=96)
          0.023702709 = weight(abstract_txt:über in 96) [ClassicSimilarity], result of:
            0.023702709 = score(doc=96,freq=2.0), product of:
              0.09023816 = queryWeight, product of:
                1.2797067 = boost
                3.9623375 = idf(docFreq=2278, maxDocs=44083)
                0.017796243 = queryNorm
              0.26266834 = fieldWeight in 96, product of:
                1.4142135 = tf(freq=2.0), with freq of:
                  2.0 = termFreq=2.0
                3.9623375 = idf(docFreq=2278, maxDocs=44083)
                0.046875 = fieldNorm(doc=96)
          0.18217617 = weight(abstract_txt:mathematik in 96) [ClassicSimilarity], result of:
            0.18217617 = score(doc=96,freq=4.0), product of:
              0.27893904 = queryWeight, product of:
                2.2499352 = boost
                6.9664416 = idf(docFreq=112, maxDocs=44083)
                0.017796243 = queryNorm
              0.6531039 = fieldWeight in 96, product of:
                2.0 = tf(freq=4.0), with freq of:
                  4.0 = termFreq=4.0
                6.9664416 = idf(docFreq=112, maxDocs=44083)
                0.046875 = fieldNorm(doc=96)
        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.13709234 = sum of:
      0.13709234 = product of:
        0.68546164 = sum of:
          0.058458105 = weight(abstract_txt:findet in 597) [ClassicSimilarity], result of:
            0.058458105 = score(doc=597,freq=1.0), product of:
              0.117180556 = queryWeight, product of:
                1.0311649 = boost
                6.385562 = idf(docFreq=201, maxDocs=44083)
                0.017796243 = queryNorm
              0.49887204 = fieldWeight in 597, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                6.385562 = idf(docFreq=201, maxDocs=44083)
                0.078125 = fieldNorm(doc=597)
          0.026257887 = weight(abstract_txt:einer in 597) [ClassicSimilarity], result of:
            0.026257887 = score(doc=597,freq=1.0), product of:
              0.086591564 = queryWeight, product of:
                1.2535831 = boost
                3.8814514 = idf(docFreq=2470, maxDocs=44083)
                0.017796243 = queryNorm
              0.3032384 = fieldWeight in 597, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                3.8814514 = idf(docFreq=2470, maxDocs=44083)
                0.078125 = fieldNorm(doc=597)
          0.10580071 = weight(abstract_txt:mathematischen in 597) [ClassicSimilarity], result of:
            0.10580071 = score(doc=597,freq=1.0), product of:
              0.1740276 = queryWeight, product of:
                1.2566358 = boost
                7.7818065 = idf(docFreq=49, maxDocs=44083)
                0.017796243 = queryNorm
              0.6079536 = fieldWeight in 597, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                7.7818065 = idf(docFreq=49, maxDocs=44083)
                0.078125 = fieldNorm(doc=597)
          0.039504517 = weight(abstract_txt:über in 597) [ClassicSimilarity], result of:
            0.039504517 = score(doc=597,freq=2.0), product of:
              0.09023816 = queryWeight, product of:
                1.2797067 = boost
                3.9623375 = idf(docFreq=2278, maxDocs=44083)
                0.017796243 = queryNorm
              0.4377806 = fieldWeight in 597, product of:
                1.4142135 = tf(freq=2.0), with freq of:
                  2.0 = termFreq=2.0
                3.9623375 = idf(docFreq=2278, maxDocs=44083)
                0.078125 = fieldNorm(doc=597)
          0.45544043 = weight(abstract_txt:mathematik in 597) [ClassicSimilarity], result of:
            0.45544043 = score(doc=597,freq=9.0), product of:
              0.27893904 = queryWeight, product of:
                2.2499352 = boost
                6.9664416 = idf(docFreq=112, maxDocs=44083)
                0.017796243 = queryNorm
              1.6327597 = fieldWeight in 597, product of:
                3.0 = tf(freq=9.0), with freq of:
                  9.0 = termFreq=9.0
                6.9664416 = idf(docFreq=112, maxDocs=44083)
                0.078125 = fieldNorm(doc=597)
        0.2 = coord(5/25)
    
  4. Nohr, H.: Rechnergestützte Gruppenarbeit : Computer-Supported Cooperative Work (CSCW) (2004) 0.14
    0.1363777 = sum of:
      0.1363777 = product of:
        1.1364809 = sum of:
          0.054068588 = weight(abstract_txt:grundlagen in 3941) [ClassicSimilarity], result of:
            0.054068588 = score(doc=3941,freq=1.0), product of:
              0.111238666 = queryWeight, product of:
                1.0046811 = boost
                6.221559 = idf(docFreq=237, maxDocs=44083)
                0.017796243 = queryNorm
              0.4860593 = fieldWeight in 3941, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                6.221559 = idf(docFreq=237, maxDocs=44083)
                0.078125 = fieldNorm(doc=3941)
          0.036087297 = weight(abstract_txt:computer in 3941) [ClassicSimilarity], result of:
            0.036087297 = score(doc=3941,freq=1.0), product of:
              0.10703817 = queryWeight, product of:
                1.3937494 = boost
                4.315446 = idf(docFreq=1600, maxDocs=44083)
                0.017796243 = queryNorm
              0.3371442 = fieldWeight in 3941, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                4.315446 = idf(docFreq=1600, maxDocs=44083)
                0.078125 = fieldNorm(doc=3941)
          1.0463251 = weight(title_txt:rechnergestützte in 3941) [ClassicSimilarity], result of:
            1.0463251 = score(doc=3941,freq=1.0), product of:
              0.28177947 = queryWeight, product of:
                1.599024 = boost
                9.90207 = idf(docFreq=5, maxDocs=44083)
                0.017796243 = queryNorm
              3.7132764 = fieldWeight in 3941, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                9.90207 = idf(docFreq=5, maxDocs=44083)
                0.375 = fieldNorm(doc=3941)
        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.13208029 = sum of:
      0.13208029 = product of:
        0.8255018 = sum of:
          0.08477887 = weight(abstract_txt:aussagen in 2210) [ClassicSimilarity], result of:
            0.08477887 = score(doc=2210,freq=1.0), product of:
              0.15013577 = queryWeight, product of:
                1.1671923 = boost
                7.2279215 = idf(docFreq=86, maxDocs=44083)
                0.017796243 = queryNorm
              0.56468135 = fieldWeight in 2210, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                7.2279215 = idf(docFreq=86, maxDocs=44083)
                0.078125 = fieldNorm(doc=2210)
          0.10580071 = weight(abstract_txt:mathematischen in 2210) [ClassicSimilarity], result of:
            0.10580071 = score(doc=2210,freq=1.0), product of:
              0.1740276 = queryWeight, product of:
                1.2566358 = boost
                7.7818065 = idf(docFreq=49, maxDocs=44083)
                0.017796243 = queryNorm
              0.6079536 = fieldWeight in 2210, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                7.7818065 = idf(docFreq=49, maxDocs=44083)
                0.078125 = fieldNorm(doc=2210)
          0.15181348 = weight(abstract_txt:mathematik in 2210) [ClassicSimilarity], result of:
            0.15181348 = score(doc=2210,freq=1.0), product of:
              0.27893904 = queryWeight, product of:
                2.2499352 = boost
                6.9664416 = idf(docFreq=112, maxDocs=44083)
                0.017796243 = queryNorm
              0.54425323 = fieldWeight in 2210, product of:
                1.0 = tf(freq=1.0), with freq of:
                  1.0 = termFreq=1.0
                6.9664416 = idf(docFreq=112, maxDocs=44083)
                0.078125 = fieldNorm(doc=2210)
          0.48310876 = weight(abstract_txt:beweisen in 2210) [ClassicSimilarity], result of:
            0.48310876 = score(doc=2210,freq=2.0), product of:
              0.4789855 = queryWeight, product of:
                2.9483328 = boost
                9.1288805 = idf(docFreq=12, maxDocs=44083)
                0.017796243 = queryNorm
              1.0086083 = fieldWeight in 2210, product of:
                1.4142135 = tf(freq=2.0), with freq of:
                  2.0 = termFreq=2.0
                9.1288805 = idf(docFreq=12, maxDocs=44083)
                0.078125 = fieldNorm(doc=2210)
        0.16 = coord(4/25)