Die Mathe-Redaktion - 15.12.2017 17:10 - Registrieren/Login
Auswahl
ListenpunktHome
ListenpunktAktuell und Interessant ai
ListenpunktArtikelübersicht/-suche
ListenpunktAlle Links / Mathe-Links
ListenpunktFach- & Sachbücher
ListenpunktMitglieder / Karte
ListenpunktRegistrieren/Login
ListenpunktArbeitsgruppen
ListenpunktSchwätz / Top 15
ListenpunktWerde Mathe-Millionär!
ListenpunktFormeleditor fedgeo
Schwarzes Brett
Aktion im Forum
Suche
Stichwortsuche in Artikeln und Links von Matheplanet
Suchen im Forum
Suchtipps

Bücher
Englische Bücher
Software
Suchbegriffe:
Mathematik bei amazon
Naturwissenschaft & Technik
In Partnerschaft mit Amazon.de
Kontakt
Mail an Matroid
[Keine Übungsaufgaben!]
Impressum

Bitte beachten Sie unsere Nutzungsbedingungen, die Distanzierung, unsere Datenschutzerklärung und
die Forumregeln.

Sie können Mitglied werden oder den Newsletter bestellen.

Der Newsletter Okt. 2017

Für Mitglieder
Mathematisch für Anfänger
Wer ist Online
Aktuell sind 616 Gäste und 28 Mitglieder online.

Sie können Mitglied werden:
Klick hier.

Über Matheplanet
 
Zum letzten Themenfilter: Themenfilter:
Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Mathematik » Logik, Mengen & Beweistechnik » Beweis durch Computerprogramm
Druckversion
Druckversion
Antworten
Antworten
Autor
Kein bestimmter Bereich Beweis durch Computerprogramm
Kiji42
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 11.10.2017
Mitteilungen: 38
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Themenstart: 2017-11-11


Hallo zusammen

Ich frage mich gerade, ob es möglich ist, dass ein Computer einen Mathematischen Beweis durchführt, wie z.B ein Theorem zu beweisen.

Liebe Grüsse

kiji



  Profil  Quote  Link auf diesen Beitrag Link
PrinzessinEinhorn
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 23.01.2017
Mitteilungen: 1025
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.1, eingetragen 2017-11-11


Hallo,

ja das ist möglich.
Ein Beispiel ist etwa der vier-Farben-Satz.

Ich habe hier im Forum auch schon öfters einen Verweis auf ein Programm "Coq" gesehen, das glaube ich auch in der Lage ist formale Beweise zu führen.

Aber Tactac kann dir da sicher mehr erzählen. :)



  Profil  Quote  Link auf diesen Beitrag Link
Kiji42
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 11.10.2017
Mitteilungen: 38
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.2, vom Themenstarter, eingetragen 2017-11-11


Danke  smile




  Profil  Quote  Link auf diesen Beitrag Link
asdfusername
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 18.03.2017
Mitteilungen: 229
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, eingetragen 2017-11-11


Hier mal zum Beispiel ein Beweis, den Coq alleine führen kann:

Theorem example (A : Set) (P : A -> Prop): ~ (exists a, P a) <-> forall a, ~ (P a).
Proof.
firstorder.
Qed.

Die zu zeigende Aussage ist <math>\neg\exists a\in A (P(a))\iff \forall a \in A(\neg (P(a)))</math>.



  Profil  Quote  Link auf diesen Beitrag Link
endy
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 10.01.2011
Mitteilungen: 3016
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.4, eingetragen 2017-11-11


Hallo.

Hier sind einmal 2 Beispiele :
mathematica
(* In *)
Clear @ "Global`*"
a[b_] := Sum[j^2, {j, 0, n}]
b[n_] := Sum[Binomial[n, k], {k, 0, n}]
a @ n
b @ n
(* Out *)
1/6 n (1 + n) (1 + 2 n)
2^n

a wird mit Gosper bewiesen,siehe Gosper.

und b mit dem Zeilberger Algorithmus,siehe Zeilberger.

Gruß endy



-----------------
Jonathan Borwein : 20.05.1951 - 02.08.2016



  Profil  Quote  Link auf diesen Beitrag Link
Kiji42
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 11.10.2017
Mitteilungen: 38
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.5, vom Themenstarter, eingetragen 2017-11-11


Danke euch :-)



  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 927
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.6, eingetragen 2017-11-11


Computerprogramme können nicht nur Beweise finden, sondern auch Programme.
Hier mal ein etwas größeres Beispiel, das das im Prinzip völlig automatisch löst. (Also, überall steht auto oder firstorder).

Record Functorial{F: Type -> Type}(map: forall{X Y}, (X -> Y) -> F X -> F Y) := {
  preserve_id X (x: F X): map (fun x => x) x = x;
  preserve_cmp X Y Z (f: Y -> Z) (g: X -> Y) (x: F X): map (fun x => f (g x)) x = map f (map g x)
}.
 
Variable R: Type.
 
Definition K A := (A -> R) -> R.
Definition J A := (A -> R) -> A.
 
Definition Kmap{A B: Type}: (A -> B) -> K A -> K B. firstorder. Defined.
 
Definition Jmap{A B: Type}: (A -> B) -> J A -> J B. firstorder. Defined.
 
Theorem KFunctorial: Functorial (@Kmap).
Proof. split; auto. Qed.
 
Theorem JFunctorial: Functorial (@Jmap).
Proof. split; auto. Qed.
 
(* natural transformation eta *)
Definition Keta(A: Type): A -> K A. firstorder. Defined.
Definition Jeta(A: Type): A -> J A. firstorder. Defined.
 
Theorem Keta_natural(A B: Type)(f: A -> B)(x: A): Keta B (f x) = Kmap f (Keta A x).
Proof. firstorder. Qed.
 
Theorem Jeta_natural(A B: Type)(f: A -> B)(x: A): Jeta B (f x) = Jmap f (Jeta A x).
Proof. firstorder. Qed.
 
(* natural transformation mu *)
Definition Kmu(A: Type): K (K A) -> K A. firstorder. Defined.
Definition Jmu(A: Type): J (J A) -> J A. firstorder. Defined.
 
Theorem Kmu_natural(A B: Type)(f: A -> B)(x: K (K A)): Kmu B (Kmap (Kmap f) x) = Kmap f (Kmu A x).
Proof. firstorder. Qed.
 
Theorem Jmu_natural(A B: Type)(f: A -> B)(x: J (J A)): Jmu B (Jmap (Jmap f) x) = Jmap f (Jmu A x).
Proof. firstorder. Qed.
 
(* monad laws *)
Theorem Keta_law1(A: Type)(x: K A): Kmu A (Kmap (Keta A) x) = x.
Proof. firstorder. Qed.
 
Theorem Jeta_law1(A: Type)(x: J A): Jmu A (Jmap (Jeta A) x) = x.
Proof. firstorder. Qed.
 
Theorem Keta_law2(A: Type)(x: K A): Kmu A (Keta (K A) x) = x.
Proof. firstorder. Qed.
 
Theorem Jeta_law2(A: Type)(x: J A): Jmu A (Jeta (J A) x) = x.
Proof. firstorder. Qed.
 
Theorem Kmu_law(A: Type)(x: K (K (K A))): Kmu A (Kmap (Kmu A) x) = Kmu A (Kmu (K A) x).
Proof. firstorder. Qed.
 
Theorem Jmu_law(A: Type)(x: J (J (J A))): Jmu A (Jmap (Jmu A) x) = Jmu A (Jmu (J A) x).
Proof. firstorder. Qed.
 
(* Test whether the found implementations are the "right" ones *)
Theorem Test0 A B (f: A -> B) x P: Kmap f x P = x (fun y => P (f y)).
Proof. firstorder. Qed.
Theorem Test1 A B (f: A -> B) x P: Jmap f x P = f (x (fun y => P (f y))).
Proof. firstorder. Qed.
 
Theorem Test2 A x P: Keta A x P = P x.
Proof. firstorder. Qed. 
Theorem Test3 A x P: Jeta A x P = x.
Proof. firstorder. Qed.
 
Theorem Test4 A x P: Kmu A x P = x (fun y => y P).
Proof. firstorder. Qed.
Theorem Test5 A x P: Jmu A x P = x (fun y => P (y P) ) P.
Proof. firstorder. Qed.
 



  Profil  Quote  Link auf diesen Beitrag Link
asdfusername
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 18.03.2017
Mitteilungen: 229
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.7, eingetragen 2017-11-11


Krass!



  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 117
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.8, eingetragen 2017-11-17 23:05


2017-11-11 14:27 - PrinzessinEinhorn in Beitrag No. 1 schreibt:
ja das ist möglich.
Ein Beispiel ist etwa der vier-Farben-Satz.

Das ist kein gutes Beispiel: Im Beweis müssen sehr viele Fallunterscheidungen betrachtet werden, womit Mathematiker aufgrund der Quantität nicht zu Rande kamen. Daher der Computereinsatz mit dem die zahlreichen Fälle dann "durchgerechnet" wurden. Also ein quantitatives Problem, im Gegensatz zu einem "mathematischen/intelektuellen Problem" wie etwa beim Beweis des großen Fermat (durch einen Menschen).

2017-11-11 14:43 - asdfusername in Beitrag No. 3 schreibt:
Hier mal zum Beispiel ein Beweis, den Coq alleine führen kann:

Theorem example (A : Set) (P : A -> Prop): ~ (exists a, P a) <-> forall a, ~ (P a).
Proof.
firstorder.
Qed.

Die zu zeigende Aussage ist <math>\neg\exists a\in A (P(a))\iff \forall a \in A(\neg (P(a)))</math>.

Das ist trivial - sowas konnten Rechner schon vor 50 Jahren (da kann Coq schon wesentlich Anspruchsvolleres).

Hier findet man beispielsweise eine Liste von Beweisaufgaben, die mit Hilfe eines Computerprogramms gelöst wurden.

"Mit Hilfe" heißt, daß das i.A. nicht automatisch klappt (solche Beweisprogramme kann es prinzipiell gar nicht geben). Dort, wo das Programm von selbst nicht weiterkommt, muß der Benutzer dann Hilfestellung geben, beispielsweise durch Angabe einer anzuwendenden Beweisregel oder durch Formulierung eines Hilfslemmas. Je weniger Hilfestellung generell erforderlich ist, desto "besser" ist solch eine Beweisprogramm.

Man kann mit so einem Programm natürlich auch Beweise für gestellte Übungsaufgaben finden. Aber man muß sich in Mathematik und Logik schon etwas auskennen, sonst klappt das nicht. Wer 12345/6789 nicht mit Papier und Bleistift ausrechnen kann, der nimmt eben einen Taschenrechner. Wer jedoch mit Papier und Bleistift nicht

fed-Code einblenden
beweisen kann, der wird mit einem Beweisprogramm nicht weit kommen.

Kurzum: Ein leistungsfähiges Werkzeug erfordert eben auch eine gewisse Expertise des Benutzer.



  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 927
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.9, eingetragen 2017-11-18 02:04


2017-11-17 23:05 - Zwerg_Allwissend in Beitrag No. 8 schreibt:
"Mit Hilfe" heißt, daß das i.A. nicht automatisch klappt (solche Beweisprogramme kann es prinzipiell gar nicht geben). Dort, wo das Programm von selbst nicht weiterkommt, muß der Benutzer dann Hilfestellung geben, beispielsweise durch Angabe einer anzuwendenden Beweisregel oder durch Formulierung eines Hilfslemmas. Je weniger Hilfestellung generell erforderlich ist, desto "besser" ist solch eine Beweisprogramm.
Ich würde sagen, man sollte sich schon möglichst auf Vollautomatik beschränken, wenn man sagen will, was Computerprogramme "können". Wenn sie jederzeit nachfragen und auf Eingaben warten dürften, könnte man auch sagen, MS Word sei in der Lage, spannende Romane zu schreiben. Festzulegen, wo denn die Grenze genau sein soll (wenn nicht bei 0), ist müßig.



  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 117
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.10, eingetragen 2017-11-18 13:36


2017-11-18 02:04 - tactac in Beitrag No. 9 schreibt:
2017-11-17 23:05 - Zwerg_Allwissend in Beitrag No. 8 schreibt:
"Mit Hilfe" heißt, daß das i.A. nicht automatisch klappt (solche Beweisprogramme kann es prinzipiell gar nicht geben). Dort, wo das Programm von selbst nicht weiterkommt, muß der Benutzer dann Hilfestellung geben, beispielsweise durch Angabe einer anzuwendenden Beweisregel oder durch Formulierung eines Hilfslemmas. Je weniger Hilfestellung generell erforderlich ist, desto "besser" ist solch eine Beweisprogramm.
Ich würde sagen, man sollte sich schon möglichst auf Vollautomatik beschränken, wenn man sagen will, was Computerprogramme "können". Wenn sie jederzeit nachfragen und auf Eingaben warten dürften, könnte man auch sagen, MS Word sei in der Lage, spannende Romane zu schreiben. Festzulegen, wo denn die Grenze genau sein soll (wenn nicht bei 0), ist müßig.

Es geht hier um ein höchst aktives Wissenschaftsgebiet mit einer Vielzahl von Konferenzen, Fachzeitschriften, Lehr- und Fachbüchern u.s.w. Wer sich dafür interessiert googelt einfach mal nach

- Automated Reasoning,
- Formal Reasoning,
- Computational Logic,
- Theorem Proving,
- Automated Theorem Proving,
- Automated Deduction,
- Computer aided Verification,
- ...

um mal einen ersten Eindruck zu gewinnen, worum es dabei überhaupt geht. Ich denke, danach hat sich der Vergleich mit MS Word von selbst erledigt.  



  Profil  Quote  Link auf diesen Beitrag Link
trunx
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 16.08.2003
Mitteilungen: 2681
Aus: Berlin
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.11, eingetragen 2017-11-18 14:03


Der Vergleich mit MS Word ist vielleicht etwas unglücklich, es gibt mittlerweile einige Ghostwriter-Programme, die durchaus in der Lage sind, aus einer "Aufgabenstellung" heraus ganze Romane zu erzeugen (ob diese dann wirklich spannend sind, ist eine andere Frage). Im Grunde geht es hier wie dort um stets wiederkehrende, also formalisier- und daher auch automatisierbare Strukturen/Abläufe.


-----------------
das problem des menschen ist nicht, dass er fleisch von tieren isst, sondern dass er für sein wachstum KRIEG gegen alle anderen lebensformen führt. dieser krieg nennt sich (land)wirtschaft, seine ideologische legitimation kultur.



  Profil  Quote  Link auf diesen Beitrag Link
asdfusername
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 18.03.2017
Mitteilungen: 229
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.12, eingetragen 2017-11-18 14:12


2017-11-18 13:36 - Zwerg_Allwissend in Beitrag No. 10 schreibt:
2017-11-18 02:04 - tactac in Beitrag No. 9 schreibt:
2017-11-17 23:05 - Zwerg_Allwissend in Beitrag No. 8 schreibt:
"Mit Hilfe" heißt, daß das i.A. nicht automatisch klappt (solche Beweisprogramme kann es prinzipiell gar nicht geben). Dort, wo das Programm von selbst nicht weiterkommt, muß der Benutzer dann Hilfestellung geben, beispielsweise durch Angabe einer anzuwendenden Beweisregel oder durch Formulierung eines Hilfslemmas. Je weniger Hilfestellung generell erforderlich ist, desto "besser" ist solch eine Beweisprogramm.
Ich würde sagen, man sollte sich schon möglichst auf Vollautomatik beschränken, wenn man sagen will, was Computerprogramme "können". Wenn sie jederzeit nachfragen und auf Eingaben warten dürften, könnte man auch sagen, MS Word sei in der Lage, spannende Romane zu schreiben. Festzulegen, wo denn die Grenze genau sein soll (wenn nicht bei 0), ist müßig.

Es geht hier um ein höchst aktives Wissenschaftsgebiet mit einer Vielzahl von Konferenzen, Fachzeitschriften, Lehr- und Fachbüchern u.s.w. Wer sich dafür interessiert googelt einfach mal nach

- Automated Reasoning,
- Formal Reasoning,
- Computational Logic,
- Theorem Proving,
- Automated Theorem Proving,
- Automated Deduction,
- Computer aided Verification,
- ...

um mal einen ersten Eindruck zu gewinnen, worum es dabei überhaupt geht. Ich denke, danach hat sich der Vergleich mit MS Word von selbst erledigt.  

Du kommst mir ziemlich arrogant vor. tactac ist ein Experte auf vielen der von dir genannten Gebieten.



  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 927
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.13, eingetragen 2017-11-18 16:10


2017-11-18 14:03 - trunx in Beitrag No. 11 schreibt:
Der Vergleich mit MS Word ist vielleicht etwas unglücklich, es gibt mittlerweile einige Ghostwriter-Programme, die durchaus in der Lage sind, aus einer "Aufgabenstellung" heraus ganze Romane zu erzeugen (ob diese dann wirklich spannend sind, ist eine andere Frage). Im Grunde geht es hier wie dort um stets wiederkehrende, also formalisier- und daher auch automatisierbare Strukturen/Abläufe.
MS Word (man hätte auch Notepad nehmen können oder eine mechanische Schreibmaschine) war ein Extrembeispiel, bei dem klar wird, dass das Erlauben von Nachfragen um Hilfe die Behauptung zweifelhaft macht, ein Programm hätte etwas geleistet. Wenn man das Beispiel unzulässig machen will, muss man eben einschränken. Letztlich wird die Einschränkung aber ziemlich beliebig bleiben.
Objektiv sinnvoll ist es, sich darauf zu konzentrieren, was zwischen den Nachfragen geleistet wird -- das ist dann aber per Definition etwas ohne Nachfragen. Im MS-Word-Beispiel kann man dann nicht mehr sagen, dass es in der Lage ist, spannende Romane zu schreiben, sondern nur noch: MS-Word kann Text anhand von Benutzereingaben manipulieren.
...und Beweisassistenten können eben Beweisteile generieren, die auch ganze Beweise sein können. Ein größerer Beweis, der nur durch Nachfragen generiert werden konnte, zählt sinnvollerweise nicht als durch den Assistenten erzeugt.



  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 117
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.14, eingetragen 2017-11-19 15:38


Ich habe mich an der Forderung aus Beitrag No.9

"Ich würde sagen, man sollte sich schon möglichst auf Vollautomatik beschränken, wenn man sagen will, was Computerprogramme "können". "

gestört, denn das klingt ja so wie: "Ein System, das Probleme nicht vollautomatisch löst, ist unbrauchbar."

Generell werden Maschinen (also auch Rechner) eingesetzt, um
(1) menschliche Arbeit einzusparen, und/oder
(2) ein qualitativ höherwertiges Ergebnis zu erzielen, und/oder
(3) die Lösung einer Aufgabe überhaupt erst zu ermöglichen.

Das sind die Kriterien für die Sinnhaftigkeit des Einsatzes von Maschinen. Würde man sich generell "auf Vollautomatik beschränken", so würde man einen Großteil des Nutzens von Maschinen verlieren.

Für die Mathematik (formale Logik) heißt das:

- Aussagenlogik ist entscheidbar, ein Rechner kann also "vollautomatisch" bestimmen, ob eine Behauptung wahr oder falsch ist.

- Prädikatenlogik erster Stufe ist nur semi-entscheidbar, d.h. es gibt korrekte und vollständige Kalküle und damit kann ein Rechner "vollautomatisch" einen Beweis für eine wahre Behauptung berechnen.

Aber was ist mit dem Rest, etwa mit der Arithmetik? Die ist noch nicht einmal semi-entscheidbar. D.h., für jedes korrekte Beweissystem gibt es wahre Behauptungen, die das System nicht beweisen kann. Also hier kann es keine "Vollautomatik" geben. Trotzdem kann man Programme schreiben, die versuchen solche Beweise zu führen. Diese Programme müssen jedoch gelegentlich scheitern. Dann gibt der Benutzer eine Hilfestellung, und das Programm arbeitet weiter bis zur nächsten Hilfestellung usw., bis ein Beweis gefunden ist.

2017-11-18 16:10 - tactac in Beitrag No. 13 schreibt:
Ein größerer Beweis, der nur durch Nachfragen generiert werden konnte, zählt sinnvollerweise nicht als durch den Assistenten erzeugt.

Das würde man seriöserweise auch nicht behaupten sondern sagen, daß solch ein Beweis "mit Unterstützung" eines Beweisassistenten berechnet wurde.

Wie schon in Beitrag No.8 geschrieben bemißt sich die Leistungsfähigkeit eines solchen Beweisassistenten  dann an der Anzahl der benötigten Hilfestellungen. Denn alles, was zwischen zwei Nachfragen geschieht, geschieht per se vollautomatisch und definiert damit, was solch ein Computerprogramm "kann".

Kurzum: Je weniger Hilfestellung erforderlich ist, desto mehr "kann" das Programm (jeweils relativ zur gestellten Aufgabe).



  Profil  Quote  Link auf diesen Beitrag Link
asdfusername
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 18.03.2017
Mitteilungen: 229
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.15, eingetragen 2017-11-19 17:45


@Zwerg_Allwissend:

1. Ein kleiner Tipp: Wenn du A seriös widerlegen willst, dann ist
"Das klingt ja so wie [hier falsche Interpretation von A einfügen] ..."
schon einmal ein schlechter Anfang.

2.
2017-11-19 15:38 - Zwerg_Allwissend in Beitrag No. 14 schreibt:

Ein größerer Beweis, der nur durch Nachfragen generiert werden konnte, zählt sinnvollerweise nicht als durch den Assistenten erzeugt.
Das würde man seriöserweise auch nicht behaupten sondern sagen, daß solch ein Beweis "mit Unterstützung" eines Beweisassistenten berechnet wurde.

Interessant, also wurde der Beweis für das Theorem von Green-Tao mit Unterstützung von LaTeX gefunden. Was für eine Schande, dass LaTeX nicht als Koautor von arxiv.org/pdf/math/0404188.pdf angegeben ist  eek



  Profil  Quote  Link auf diesen Beitrag Link
Kiji42 hat die Antworten auf ihre/seine Frage gesehen.
Kiji42 hatte hier bereits selbst das Ok-Häkchen gesetzt.
Kiji42 wird per Mail über neue Antworten informiert.
Neues Thema [Neues Thema] Antworten [Antworten]    Druckversion [Druckversion]

 


Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2017 by Matroids Matheplanet
This web site was made with PHP-Nuke, a web portal system written in PHP. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]