natural language proof assistant












7














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







share|cite|improve this question




















  • 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


















7














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







share|cite|improve this question




















  • 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
















7












7








7


3





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







share|cite|improve this question















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






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited May 28 '13 at 12:37

























asked May 26 '13 at 19:22









user76556

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
















  • 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












3 Answers
3






active

oldest

votes


















4














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.






share|cite|improve this answer



















  • 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



















0














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.






share|cite|improve this answer































    -1














    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?






    share|cite|improve this answer



















    • 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











    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
    });


    }
    });














    draft saved

    draft discarded


















    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









    4














    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.






    share|cite|improve this answer



















    • 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
















    4














    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.






    share|cite|improve this answer



















    • 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














    4












    4








    4






    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.






    share|cite|improve this answer














    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.







    share|cite|improve this answer














    share|cite|improve this answer



    share|cite|improve this answer








    edited Jul 16 '17 at 19:36

























    answered Jun 1 '13 at 10:02









    Musa Al-hassy

    1,3191711




    1,3191711








    • 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




      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











    0














    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.






    share|cite|improve this answer




























      0














      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.






      share|cite|improve this answer


























        0












        0








        0






        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.






        share|cite|improve this answer














        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.







        share|cite|improve this answer














        share|cite|improve this answer



        share|cite|improve this answer








        edited Nov 29 '18 at 2:03

























        answered Jul 12 '18 at 21:19









        Anderson Green

        38071122




        38071122























            -1














            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?






            share|cite|improve this answer



















            • 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














            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?






            share|cite|improve this answer



















            • 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








            -1






            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?






            share|cite|improve this answer














            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?







            share|cite|improve this answer














            share|cite|improve this answer



            share|cite|improve this answer








            edited Apr 13 '17 at 12:21









            Community♦

            1




            1










            answered May 26 '13 at 20:30









            wolfies

            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














            • 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


















            draft saved

            draft discarded




















































            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.




            draft saved


            draft discarded














            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





















































            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







            -

            Popular posts from this blog

            Probability when a professor distributes a quiz and homework assignment to a class of n students.

            Image
            0 0 $begingroup$ Need help with this problem. Suppose our lazy professor collects a quiz and a homework assignment from a class of n students one day, then distributes both the quizzes and the homework assignments back to the class in a random fashion for grading. Each student receives one quiz and one homework assignment to grade. (a) What is the probability that every student receives someone else's quiz to grade, and someone else's homework to grade? (b) What is the probability that no student receives both their own quiz and their own homework assignment to grade? In this case, some students may receive their own quiz, and others may receive their own homework assignment. (c) Compute the limiting probability as n approaches infinity in each case. ...
            Read more

            Aardman Animations

            Image
            Aardman Animations, Ltd. Aardman Animations Tipo privada Atividade Animação em stop-motion , Animação em CGI Fundação 1972 Fundador(es) Peter Lord David Sproxton Sede Bristol, Inglaterra  Reino Unido Proprietário(s) Dreamworks Pessoas-chave Peter Lord David Sproxton Nick Park Divisões Aardman Features Aardman Digital Aardman Commercials Aardman Broadcast Aardman International Aardman Rights Aardman Effects Aardman 3-D Systems Aardman Nathan Love AardBoiled Website oficial aardman.com ...
            Read more

            Are they similar matrix

            Image
            0 $begingroup$ Do $begin{bmatrix} 0&i&0\0&0&1\0&0&0 end{bmatrix} $ and $begin{bmatrix} 0&0&0\-i&0&0\0&1&0 end{bmatrix} $ are similar.Is this True/false Clearly both are nilpotent and one is conjucate transpose of other but how to know if they are similar.i'm stuck. Please help me linear-algebra vector-spaces eigenvalues-eigenvectors generalizedeigenvector share | cite | improve this question edited Dec 10 '18 at 6:38 Vasanth Kris asked Dec 10 '18 at 6:19 ...
            Read more