4 ms·

Sometimes I wonder why LaTeX math mode doesn't do some fancy static analysis. Considering how much math is just a language, and we know how to prove (and check)

Sometimes I wonder why LaTeX math mode doesn't do some fancy static analysis. Considering how much math is just a language, and we know how to prove (and check) things about languages. Maybe you could automatically defend against a misspelled variable in an equation, or go much further... Are there any cool projects I'm missing out on?

puzzledobserver 7y ago
Jupyter notebooks might be a better target than Latex. One could conceivable verify proofs in the _small_, leaving some big reasoning steps out of the verification process. Then export the development to Latex, where it is automatically typeset.
wisnesky 7y ago
Kevin Redwine: Inference Rules Plus Proof-Search Strategies Equals Programs (2009). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.1250 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.... In the programming-language community many authors communicate algorithms through the use of inference rules. To get from rules to working code requires careful thought and effort. If the rules change or the author wants to use a different algorithm, the effort required to fix the code can be disproportionate to the size of the change in the rules. This thesis shows that it is possible to generate working code automatically from inference rules as they appear in publications. The method of this generation is found in the combination of two domain-specific languages: Ruletex and MonStr. Ruletex formally describes inference rules; MonStr connects the rules to an algorithm. Ruletex descriptions are embedded in LATEX, the language that researchers use to publish their work, so that the author commands complete control of the rules ’ appearance. Moreover the generated code enjoys several nice properties: Existing code written in a general-purpose programming language can interoperate with Ruletex code, correctness of rules is decoupled from performance and termination of code, and implementations are conceptually simple, consisting only of λ-calculus with pattern matching. The main technical contribution of this work is the design of MonStr, the executionstrategy language used to form an algorithm out of rules. MonStr specifications provide an important guarantee: a valid strategy cannot affect partial correctness, although it can affect termination, completeness, and efficiency.
stephenSinniah 7y ago
I was watching a video by Kevin Buzzard, he talks about using Lean Theorem Prover, seems pretty interesting https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE
- baby 7y ago
  I watched that the other day and this is the most inspiring, maybe potentially ground breaking video I’ve seen in the last decade. That’s the first time I watched something and thought, this is probably the future. This is the start of something that will have repercussion in the next thousand of years. I recommend this paper from Lamport on how to write a 21st century proof: https://lamport.azurewebsites.net/pubs/proof.pdf https://lamport.azurewebsites.net/pubs/proof.pdf
joycian 7y ago
Well, there is the Naproche-SAD project: https://github.com/Naproche/Naproche-SAD/blob/master/README.md https://github.com/Naproche/Naproche-SAD/blob/master/README.... > Proof Checking of Natural Mathematical Documents, with optional support for Isabelle Prover IDE. The goal is to be able to proofcheck from Latex directly. Most of the machinery is (used to be) written in Haskell. It is definitely a cool project, and they could definitely use help.
seanwilson 7y ago
> Sometimes I wonder why LaTeX math mode doesn't do some fancy static analysis. Considering how much math is just a language, and we know how to prove (and check) things about languages It wouldn't be practical beyond some basic checks. Turning a paper proof from even the standard you'd find in a journal publication into a formalised (e.g. Coq) proof is a research grade task. The automation required to justify each step in a typical paper proof back to your axioms isn't close to being practical for casual use.

puzzledobserver 7y ago

Jupyter notebooks might be a better target than Latex. One could conceivable verify proofs in the _small_, leaving some big reasoning steps out of the verification process. Then export the development to Latex, where it is automatically typeset.

wisnesky 7y ago

Kevin Redwine: Inference Rules Plus Proof-Search Strategies Equals Programs (2009). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.1250 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.... In the programming-language community many authors communicate algorithms through the use of inference rules. To get from rules to working code requires careful thought and effort. If the rules change or the author wants to use a different algorithm, the effort required to fix the code can be disproportionate to the size of the change in the rules. This thesis shows that it is possible to generate working code automatically from inference rules as they appear in publications. The method of this generation is found in the combination of two domain-specific languages: Ruletex and MonStr. Ruletex formally describes inference rules; MonStr connects the rules to an algorithm. Ruletex descriptions are embedded in LATEX, the language that researchers use to publish their work, so that the author commands complete control of the rules ’ appearance. Moreover the generated code enjoys several nice properties: Existing code written in a general-purpose programming language can interoperate with Ruletex code, correctness of rules is decoupled from performance and termination of code, and implementations are conceptually simple, consisting only of λ-calculus with pattern matching. The main technical contribution of this work is the design of MonStr, the executionstrategy language used to form an algorithm out of rules. MonStr specifications provide an important guarantee: a valid strategy cannot affect partial correctness, although it can affect termination, completeness, and efficiency.

stephenSinniah 7y ago

I was watching a video by Kevin Buzzard, he talks about using Lean Theorem Prover, seems pretty interesting https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE

baby 7y ago
I watched that the other day and this is the most inspiring, maybe potentially ground breaking video I’ve seen in the last decade. That’s the first time I watched something and thought, this is probably the future. This is the start of something that will have repercussion in the next thousand of years. I recommend this paper from Lamport on how to write a 21st century proof: https://lamport.azurewebsites.net/pubs/proof.pdf https://lamport.azurewebsites.net/pubs/proof.pdf

joycian 7y ago

Well, there is the Naproche-SAD project: https://github.com/Naproche/Naproche-SAD/blob/master/README.md https://github.com/Naproche/Naproche-SAD/blob/master/README.... > Proof Checking of Natural Mathematical Documents, with optional support for Isabelle Prover IDE. The goal is to be able to proofcheck from Latex directly. Most of the machinery is (used to be) written in Haskell. It is definitely a cool project, and they could definitely use help.

seanwilson 7y ago

> Sometimes I wonder why LaTeX math mode doesn't do some fancy static analysis. Considering how much math is just a language, and we know how to prove (and check) things about languages It wouldn't be practical beyond some basic checks. Turning a paper proof from even the standard you'd find in a journal publication into a formalised (e.g. Coq) proof is a research grade task. The automation required to justify each step in a typical paper proof back to your axioms isn't close to being practical for casual use.