natural language proof assistant
I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english,
I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then instead of sending it to a journal to have it verified you use the proof assistant to have it verified for you.
There are programming languages like inform7 in which you program in english. I think what is needed is a set of macro's to turn the tex into, lets say, something that Coq can verify. Is there any such thing out there?
Do you think if this happens casual mathematicians will use it? or are there deeper problems that people don't use them now??
proof-writing automated-theorem-proving theorem-provers
asked May 26 '13 at 19:22
user76556user76556
418210
add a comment |
I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english,
I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then instead of sending it to a journal to have it verified you use the proof assistant to have it verified for you.
There are programming languages like inform7 in which you program in english. I think what is needed is a set of macro's to turn the tex into, lets say, something that Coq can verify. Is there any such thing out there?
Do you think if this happens casual mathematicians will use it? or are there deeper problems that people don't use them now??
proof-writing automated-theorem-proving theorem-provers
asked May 26 '13 at 19:22
user76556user76556
418210
1
While I'm not too sure on what exactly you are asking, I feel like the series of blog posts by Tim Gowers may be of interest: gowers.wordpress.com/2013/03/25/… ; gowers.wordpress.com/2013/04/02/… ; gowers.wordpress.com/2013/04/14/…
– Andrew D
May 28 '13 at 9:37
thanks. unfortunately my internet is filtered. wordpress is not accessible in iran. do you know where else i can get this posts? i'll edit my question to make it more clear.
– user76556
May 28 '13 at 12:30
1
Ah, I thought you meant a computer proving theorems in a natural language, rather than a proof checker which can check proofs in a natural language. Regardless, if you're also interested in the former, I can send you the content of the posts.
– Andrew D
May 28 '13 at 13:37
add a comment |
I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english,
I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then instead of sending it to a journal to have it verified you use the proof assistant to have it verified for you.
There are programming languages like inform7 in which you program in english. I think what is needed is a set of macro's to turn the tex into, lets say, something that Coq can verify. Is there any such thing out there?
Do you think if this happens casual mathematicians will use it? or are there deeper problems that people don't use them now??
proof-writing automated-theorem-proving theorem-provers
asked May 26 '13 at 19:22
user76556user76556
418210
I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english,
I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then instead of sending it to a journal to have it verified you use the proof assistant to have it verified for you.
There are programming languages like inform7 in which you program in english. I think what is needed is a set of macro's to turn the tex into, lets say, something that Coq can verify. Is there any such thing out there?
Do you think if this happens casual mathematicians will use it? or are there deeper problems that people don't use them now??
proof-writing automated-theorem-proving theorem-provers
proof-writing automated-theorem-proving theorem-provers
asked May 26 '13 at 19:22
user76556user76556
418210
asked May 26 '13 at 19:22
user76556user76556
418210
edited May 28 '13 at 12:37
user76556
asked May 26 '13 at 19:22
user76556user76556
418210
asked May 26 '13 at 19:22
user76556user76556
418210
asked May 26 '13 at 19:22
user76556user76556
418210
418210
1
While I'm not too sure on what exactly you are asking, I feel like the series of blog posts by Tim Gowers may be of interest: gowers.wordpress.com/2013/03/25/… ; gowers.wordpress.com/2013/04/02/… ; gowers.wordpress.com/2013/04/14/…
– Andrew D
May 28 '13 at 9:37
thanks. unfortunately my internet is filtered. wordpress is not accessible in iran. do you know where else i can get this posts? i'll edit my question to make it more clear.
– user76556
May 28 '13 at 12:30
1
Ah, I thought you meant a computer proving theorems in a natural language, rather than a proof checker which can check proofs in a natural language. Regardless, if you're also interested in the former, I can send you the content of the posts.
– Andrew D
May 28 '13 at 13:37
add a comment |
1
While I'm not too sure on what exactly you are asking, I feel like the series of blog posts by Tim Gowers may be of interest: gowers.wordpress.com/2013/03/25/… ; gowers.wordpress.com/2013/04/02/… ; gowers.wordpress.com/2013/04/14/…
– Andrew D
May 28 '13 at 9:37
thanks. unfortunately my internet is filtered. wordpress is not accessible in iran. do you know where else i can get this posts? i'll edit my question to make it more clear.
– user76556
May 28 '13 at 12:30
1
Ah, I thought you meant a computer proving theorems in a natural language, rather than a proof checker which can check proofs in a natural language. Regardless, if you're also interested in the former, I can send you the content of the posts.
– Andrew D
May 28 '13 at 13:37
1
1
While I'm not too sure on what exactly you are asking, I feel like the series of blog posts by Tim Gowers may be of interest: gowers.wordpress.com/2013/03/25/… ; gowers.wordpress.com/2013/04/02/… ; gowers.wordpress.com/2013/04/14/…
– Andrew D
May 28 '13 at 9:37
While I'm not too sure on what exactly you are asking, I feel like the series of blog posts by Tim Gowers may be of interest: gowers.wordpress.com/2013/03/25/… ; gowers.wordpress.com/2013/04/02/… ; gowers.wordpress.com/2013/04/14/…
– Andrew D
May 28 '13 at 9:37
thanks. unfortunately my internet is filtered. wordpress is not accessible in iran. do you know where else i can get this posts? i'll edit my question to make it more clear.
– user76556
May 28 '13 at 12:30
thanks. unfortunately my internet is filtered. wordpress is not accessible in iran. do you know where else i can get this posts? i'll edit my question to make it more clear.
– user76556
May 28 '13 at 12:30
1
1
Ah, I thought you meant a computer proving theorems in a natural language, rather than a proof checker which can check proofs in a natural language. Regardless, if you're also interested in the former, I can send you the content of the posts.
– Andrew D
May 28 '13 at 13:37
Ah, I thought you meant a computer proving theorems in a natural language, rather than a proof checker which can check proofs in a natural language. Regardless, if you're also interested in the former, I can send you the content of the posts.
– Andrew D
May 28 '13 at 13:37
add a comment |
3 Answers
3
active
oldest
votes
The proof-checker CalcCheck takes input via $TeX{}$ in the form of formulas and
accompanying English hints/justifications.
Given the input file, the system will output that the proof is valid at all steps or indicate which steps are poorly justified.
To the best of my knowledge, it currently recognizes most theorems of first order logic and set theory ---based on the great text ``A Logical Approach to Discrete Math.''
If I recall correctly, the back-end is in Haskell or may have already moved to Agda (a system like ${bf Coq}$).
Main system site is at http://calccheck.mcmaster.ca/.
See $S 5.3$ of the manual for a application, http://calccheck.mcmaster.ca/CalcCheckManual.pdf.
On a final note, this system has been used in first-year logic courses to assist students in proof-writing. It is helpful to have a system check one's proof when in-doubt.
Best regards,
Moses
Edit The above was 2013, now as of 2017, it now supports
- creation of logical theories via named modules in the style of the Agda language
- unicode input directly via latex-style bindings
- "code completion" for theorem names and definitions
- coloured and somewhat helpful error messages.
Moreover, the system now no-longer needs to be installed as an application but can be used directly via a browser.
It has been successfully used in-place of paper-and-pencil examinations at the university level with over 200 students in the 2017 fall term alone.
answered Jun 1 '13 at 10:02
Musa Al-hassyMusa Al-hassy
1,3391711
1
it is not exactly what i was looking for. but it seems closer than the other theorem provers to what i wanted. i'll give it a try thanks.
– user76556
Jun 1 '13 at 17:47
add a comment |
There is now a program called Coqatoo that converts Coq proofs into natural-language proofs. It may be feasible to write a translator that would convert these English proofs back into Coq, but I do not know if this has been done yet.
In order to implement a natural-language theorem prover, it would be necessary to convert the input into a formal semantic representation of its meaning. The ACE reasoner was implemented in this way, using Attempto Controlled English as its input language.
answered Jul 12 '18 at 21:19
Anderson GreenAnderson Green
38071122
add a comment |
I believe the RISC (Research Institute for Symbolic Computation) group at Castle Hagenberg in Austria have been involved in such things for many years.
See: www.theorema.org
Based on the OP's comments below, it appears that they are not seeking an automated 'theorem prover', but an automated 'proof verifier'. If so, there is already a thread on this at:
How do proof verifiers work?
edited Apr 13 '17 at 12:21
Community♦
1
answered May 26 '13 at 20:30
wolfieswolfies
4,1682923
1
maybe i am wrong but it seems it is a theorem prover that generates human readable proofs. this is the opposite of what i asked.
– user76556
May 26 '13 at 20:42
what did you ask?
– wolfies
May 28 '13 at 6:59
a proof assistant that checks the proof not generates one. but it's input is a proof written in english. like a normal tex file. it's output is either 'this proof is correct' or 'this proof is incorrect'
– user76556
May 28 '13 at 9:22
the thread mentioned above is not exactly answering my question. it is more about HOW proof assistants work. and all that lambda calculus?, calculi? higher order logic? etc. i want to know about proof assistants from an end customer point of view, a casual mathematician.
– user76556
May 30 '13 at 7:56
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f403163%2fnatural-language-proof-assistant%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
The proof-checker CalcCheck takes input via $TeX{}$ in the form of formulas and
accompanying English hints/justifications.
Given the input file, the system will output that the proof is valid at all steps or indicate which steps are poorly justified.
To the best of my knowledge, it currently recognizes most theorems of first order logic and set theory ---based on the great text ``A Logical Approach to Discrete Math.''
If I recall correctly, the back-end is in Haskell or may have already moved to Agda (a system like ${bf Coq}$).
Main system site is at http://calccheck.mcmaster.ca/.
See $S 5.3$ of the manual for a application, http://calccheck.mcmaster.ca/CalcCheckManual.pdf.
On a final note, this system has been used in first-year logic courses to assist students in proof-writing. It is helpful to have a system check one's proof when in-doubt.
Best regards,
Moses
Edit The above was 2013, now as of 2017, it now supports
- creation of logical theories via named modules in the style of the Agda language
- unicode input directly via latex-style bindings
- "code completion" for theorem names and definitions
- coloured and somewhat helpful error messages.
Moreover, the system now no-longer needs to be installed as an application but can be used directly via a browser.
It has been successfully used in-place of paper-and-pencil examinations at the university level with over 200 students in the 2017 fall term alone.
answered Jun 1 '13 at 10:02
Musa Al-hassyMusa Al-hassy
1,3391711
1
it is not exactly what i was looking for. but it seems closer than the other theorem provers to what i wanted. i'll give it a try thanks.
– user76556
Jun 1 '13 at 17:47
add a comment |
The proof-checker CalcCheck takes input via $TeX{}$ in the form of formulas and
accompanying English hints/justifications.
Given the input file, the system will output that the proof is valid at all steps or indicate which steps are poorly justified.
To the best of my knowledge, it currently recognizes most theorems of first order logic and set theory ---based on the great text ``A Logical Approach to Discrete Math.''
If I recall correctly, the back-end is in Haskell or may have already moved to Agda (a system like ${bf Coq}$).
Main system site is at http://calccheck.mcmaster.ca/.
See $S 5.3$ of the manual for a application, http://calccheck.mcmaster.ca/CalcCheckManual.pdf.
On a final note, this system has been used in first-year logic courses to assist students in proof-writing. It is helpful to have a system check one's proof when in-doubt.
Best regards,
Moses
Edit The above was 2013, now as of 2017, it now supports
- creation of logical theories via named modules in the style of the Agda language
- unicode input directly via latex-style bindings
- "code completion" for theorem names and definitions
- coloured and somewhat helpful error messages.
Moreover, the system now no-longer needs to be installed as an application but can be used directly via a browser.
It has been successfully used in-place of paper-and-pencil examinations at the university level with over 200 students in the 2017 fall term alone.
answered Jun 1 '13 at 10:02
Musa Al-hassyMusa Al-hassy
1,3391711
1
it is not exactly what i was looking for. but it seems closer than the other theorem provers to what i wanted. i'll give it a try thanks.
– user76556
Jun 1 '13 at 17:47
add a comment |
The proof-checker CalcCheck takes input via $TeX{}$ in the form of formulas and
accompanying English hints/justifications.
Given the input file, the system will output that the proof is valid at all steps or indicate which steps are poorly justified.
To the best of my knowledge, it currently recognizes most theorems of first order logic and set theory ---based on the great text ``A Logical Approach to Discrete Math.''
If I recall correctly, the back-end is in Haskell or may have already moved to Agda (a system like ${bf Coq}$).
Main system site is at http://calccheck.mcmaster.ca/.
See $S 5.3$ of the manual for a application, http://calccheck.mcmaster.ca/CalcCheckManual.pdf.
On a final note, this system has been used in first-year logic courses to assist students in proof-writing. It is helpful to have a system check one's proof when in-doubt.
Best regards,
Moses
Edit The above was 2013, now as of 2017, it now supports
- creation of logical theories via named modules in the style of the Agda language
- unicode input directly via latex-style bindings
- "code completion" for theorem names and definitions
- coloured and somewhat helpful error messages.
Moreover, the system now no-longer needs to be installed as an application but can be used directly via a browser.
It has been successfully used in-place of paper-and-pencil examinations at the university level with over 200 students in the 2017 fall term alone.
answered Jun 1 '13 at 10:02
Musa Al-hassyMusa Al-hassy
1,3391711
The proof-checker CalcCheck takes input via $TeX{}$ in the form of formulas and
accompanying English hints/justifications.
Given the input file, the system will output that the proof is valid at all steps or indicate which steps are poorly justified.
To the best of my knowledge, it currently recognizes most theorems of first order logic and set theory ---based on the great text ``A Logical Approach to Discrete Math.''
If I recall correctly, the back-end is in Haskell or may have already moved to Agda (a system like ${bf Coq}$).
Main system site is at http://calccheck.mcmaster.ca/.
See $S 5.3$ of the manual for a application, http://calccheck.mcmaster.ca/CalcCheckManual.pdf.
On a final note, this system has been used in first-year logic courses to assist students in proof-writing. It is helpful to have a system check one's proof when in-doubt.
Best regards,
Moses
Edit The above was 2013, now as of 2017, it now supports
- creation of logical theories via named modules in the style of the Agda language
- unicode input directly via latex-style bindings
- "code completion" for theorem names and definitions
- coloured and somewhat helpful error messages.
Moreover, the system now no-longer needs to be installed as an application but can be used directly via a browser.
It has been successfully used in-place of paper-and-pencil examinations at the university level with over 200 students in the 2017 fall term alone.
answered Jun 1 '13 at 10:02
Musa Al-hassyMusa Al-hassy
1,3391711
edited Jul 16 '17 at 19:36
answered Jun 1 '13 at 10:02
Musa Al-hassyMusa Al-hassy
1,3391711
answered Jun 1 '13 at 10:02
Musa Al-hassyMusa Al-hassy
1,3391711
answered Jun 1 '13 at 10:02
Musa Al-hassyMusa Al-hassy
1,3391711
1,3391711
1
it is not exactly what i was looking for. but it seems closer than the other theorem provers to what i wanted. i'll give it a try thanks.
– user76556
Jun 1 '13 at 17:47
add a comment |
1
it is not exactly what i was looking for. but it seems closer than the other theorem provers to what i wanted. i'll give it a try thanks.
– user76556
Jun 1 '13 at 17:47
1
1
it is not exactly what i was looking for. but it seems closer than the other theorem provers to what i wanted. i'll give it a try thanks.
– user76556
Jun 1 '13 at 17:47
it is not exactly what i was looking for. but it seems closer than the other theorem provers to what i wanted. i'll give it a try thanks.
– user76556
Jun 1 '13 at 17:47
add a comment |
There is now a program called Coqatoo that converts Coq proofs into natural-language proofs. It may be feasible to write a translator that would convert these English proofs back into Coq, but I do not know if this has been done yet.
In order to implement a natural-language theorem prover, it would be necessary to convert the input into a formal semantic representation of its meaning. The ACE reasoner was implemented in this way, using Attempto Controlled English as its input language.
answered Jul 12 '18 at 21:19
Anderson GreenAnderson Green
38071122
add a comment |
There is now a program called Coqatoo that converts Coq proofs into natural-language proofs. It may be feasible to write a translator that would convert these English proofs back into Coq, but I do not know if this has been done yet.
In order to implement a natural-language theorem prover, it would be necessary to convert the input into a formal semantic representation of its meaning. The ACE reasoner was implemented in this way, using Attempto Controlled English as its input language.
answered Jul 12 '18 at 21:19
Anderson GreenAnderson Green
38071122
add a comment |
There is now a program called Coqatoo that converts Coq proofs into natural-language proofs. It may be feasible to write a translator that would convert these English proofs back into Coq, but I do not know if this has been done yet.
In order to implement a natural-language theorem prover, it would be necessary to convert the input into a formal semantic representation of its meaning. The ACE reasoner was implemented in this way, using Attempto Controlled English as its input language.
answered Jul 12 '18 at 21:19
Anderson GreenAnderson Green
38071122
There is now a program called Coqatoo that converts Coq proofs into natural-language proofs. It may be feasible to write a translator that would convert these English proofs back into Coq, but I do not know if this has been done yet.
In order to implement a natural-language theorem prover, it would be necessary to convert the input into a formal semantic representation of its meaning. The ACE reasoner was implemented in this way, using Attempto Controlled English as its input language.
answered Jul 12 '18 at 21:19
Anderson GreenAnderson Green
38071122
edited Nov 29 '18 at 2:03
answered Jul 12 '18 at 21:19
Anderson GreenAnderson Green
38071122
answered Jul 12 '18 at 21:19
Anderson GreenAnderson Green
38071122
answered Jul 12 '18 at 21:19
Anderson GreenAnderson Green
38071122
38071122
add a comment |
add a comment |
I believe the RISC (Research Institute for Symbolic Computation) group at Castle Hagenberg in Austria have been involved in such things for many years.
See: www.theorema.org
Based on the OP's comments below, it appears that they are not seeking an automated 'theorem prover', but an automated 'proof verifier'. If so, there is already a thread on this at:
How do proof verifiers work?
edited Apr 13 '17 at 12:21
Community♦
1
answered May 26 '13 at 20:30
wolfieswolfies
4,1682923
1
maybe i am wrong but it seems it is a theorem prover that generates human readable proofs. this is the opposite of what i asked.
– user76556
May 26 '13 at 20:42
what did you ask?
– wolfies
May 28 '13 at 6:59
a proof assistant that checks the proof not generates one. but it's input is a proof written in english. like a normal tex file. it's output is either 'this proof is correct' or 'this proof is incorrect'
– user76556
May 28 '13 at 9:22
the thread mentioned above is not exactly answering my question. it is more about HOW proof assistants work. and all that lambda calculus?, calculi? higher order logic? etc. i want to know about proof assistants from an end customer point of view, a casual mathematician.
– user76556
May 30 '13 at 7:56
add a comment |
I believe the RISC (Research Institute for Symbolic Computation) group at Castle Hagenberg in Austria have been involved in such things for many years.
See: www.theorema.org
Based on the OP's comments below, it appears that they are not seeking an automated 'theorem prover', but an automated 'proof verifier'. If so, there is already a thread on this at:
How do proof verifiers work?
edited Apr 13 '17 at 12:21
Community♦
1
answered May 26 '13 at 20:30
wolfieswolfies
4,1682923
1
maybe i am wrong but it seems it is a theorem prover that generates human readable proofs. this is the opposite of what i asked.
– user76556
May 26 '13 at 20:42
what did you ask?
– wolfies
May 28 '13 at 6:59
a proof assistant that checks the proof not generates one. but it's input is a proof written in english. like a normal tex file. it's output is either 'this proof is correct' or 'this proof is incorrect'
– user76556
May 28 '13 at 9:22
the thread mentioned above is not exactly answering my question. it is more about HOW proof assistants work. and all that lambda calculus?, calculi? higher order logic? etc. i want to know about proof assistants from an end customer point of view, a casual mathematician.
– user76556
May 30 '13 at 7:56
add a comment |
I believe the RISC (Research Institute for Symbolic Computation) group at Castle Hagenberg in Austria have been involved in such things for many years.
See: www.theorema.org
Based on the OP's comments below, it appears that they are not seeking an automated 'theorem prover', but an automated 'proof verifier'. If so, there is already a thread on this at:
How do proof verifiers work?
edited Apr 13 '17 at 12:21
Community♦
1
answered May 26 '13 at 20:30
wolfieswolfies
4,1682923
I believe the RISC (Research Institute for Symbolic Computation) group at Castle Hagenberg in Austria have been involved in such things for many years.
See: www.theorema.org
Based on the OP's comments below, it appears that they are not seeking an automated 'theorem prover', but an automated 'proof verifier'. If so, there is already a thread on this at:
How do proof verifiers work?
edited Apr 13 '17 at 12:21
Community♦
1
answered May 26 '13 at 20:30
wolfieswolfies
4,1682923
edited Apr 13 '17 at 12:21
Community♦
1
edited Apr 13 '17 at 12:21
Community♦
1
edited Apr 13 '17 at 12:21
Community♦
1
1
answered May 26 '13 at 20:30
wolfieswolfies
4,1682923
answered May 26 '13 at 20:30
wolfieswolfies
4,1682923
answered May 26 '13 at 20:30
wolfieswolfies
4,1682923
4,1682923
1
maybe i am wrong but it seems it is a theorem prover that generates human readable proofs. this is the opposite of what i asked.
– user76556
May 26 '13 at 20:42
what did you ask?
– wolfies
May 28 '13 at 6:59
a proof assistant that checks the proof not generates one. but it's input is a proof written in english. like a normal tex file. it's output is either 'this proof is correct' or 'this proof is incorrect'
– user76556
May 28 '13 at 9:22
the thread mentioned above is not exactly answering my question. it is more about HOW proof assistants work. and all that lambda calculus?, calculi? higher order logic? etc. i want to know about proof assistants from an end customer point of view, a casual mathematician.
– user76556
May 30 '13 at 7:56
add a comment |
1
maybe i am wrong but it seems it is a theorem prover that generates human readable proofs. this is the opposite of what i asked.
– user76556
May 26 '13 at 20:42
what did you ask?
– wolfies
May 28 '13 at 6:59
a proof assistant that checks the proof not generates one. but it's input is a proof written in english. like a normal tex file. it's output is either 'this proof is correct' or 'this proof is incorrect'
– user76556
May 28 '13 at 9:22
the thread mentioned above is not exactly answering my question. it is more about HOW proof assistants work. and all that lambda calculus?, calculi? higher order logic? etc. i want to know about proof assistants from an end customer point of view, a casual mathematician.
– user76556
May 30 '13 at 7:56
1
1
maybe i am wrong but it seems it is a theorem prover that generates human readable proofs. this is the opposite of what i asked.
– user76556
May 26 '13 at 20:42
maybe i am wrong but it seems it is a theorem prover that generates human readable proofs. this is the opposite of what i asked.
– user76556
May 26 '13 at 20:42
what did you ask?
– wolfies
May 28 '13 at 6:59
what did you ask?
– wolfies
May 28 '13 at 6:59
a proof assistant that checks the proof not generates one. but it's input is a proof written in english. like a normal tex file. it's output is either 'this proof is correct' or 'this proof is incorrect'
– user76556
May 28 '13 at 9:22
a proof assistant that checks the proof not generates one. but it's input is a proof written in english. like a normal tex file. it's output is either 'this proof is correct' or 'this proof is incorrect'
– user76556
May 28 '13 at 9:22
the thread mentioned above is not exactly answering my question. it is more about HOW proof assistants work. and all that lambda calculus?, calculi? higher order logic? etc. i want to know about proof assistants from an end customer point of view, a casual mathematician.
– user76556
May 30 '13 at 7:56
the thread mentioned above is not exactly answering my question. it is more about HOW proof assistants work. and all that lambda calculus?, calculi? higher order logic? etc. i want to know about proof assistants from an end customer point of view, a casual mathematician.
– user76556
May 30 '13 at 7:56
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f403163%2fnatural-language-proof-assistant%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
While I'm not too sure on what exactly you are asking, I feel like the series of blog posts by Tim Gowers may be of interest: gowers.wordpress.com/2013/03/25/… ; gowers.wordpress.com/2013/04/02/… ; gowers.wordpress.com/2013/04/14/…
– Andrew D
May 28 '13 at 9:37
thanks. unfortunately my internet is filtered. wordpress is not accessible in iran. do you know where else i can get this posts? i'll edit my question to make it more clear.
– user76556
May 28 '13 at 12:30
1
Ah, I thought you meant a computer proving theorems in a natural language, rather than a proof checker which can check proofs in a natural language. Regardless, if you're also interested in the former, I can send you the content of the posts.
– Andrew D
May 28 '13 at 13:37