/sci/ - Science & Math » Thread #13522384

96KiB, 1920x1080, screen-lesson1.png

View Same Google iqdb SauceNAO

Math, Software

Mathematical proof? What is it actually? Sun 15 Aug 16:13:58 2021 No.13522384 View Reply Original Report

Quoted By: >>13522412 >>13525508 >>13525582 >>13530966 >>13533304

What do think about systems like Lean, Coq?
What wrong with this software?
What makes it so hard to learn?

Anonymous

Anonymous Sun 15 Aug 2021 16:24:45 No.13522412 Report

Quoted By: >>13523623 >>13523662

>>13522384
Literal midwit cope
Shills should go back to rmath posting shitty threads and failing to convince us to (((open source ))) math
Its even more disrespectful to us to see cs midwits shills with no real interest in math larp on about curry howard and its usefulness??? Then post worthless threads on finding picture books to learn "harder" maths

Id rather share my research to telegram and 2ch shitposters than feddit cs midwits

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Sun 15 Aug 2021 16:30:09 No.13522430 Report

Quoted By:

I think proof is a like path in graph, that have nodes and edges.
This can be better viewed if you think about forward proof and backward proof.
Forward proof is like answer to question:
What can i have now? What can i easy get by 1 step of (replacing, rewriting or ...)?
Forward proof - just one step from current state of knowledge.
Example:
Prove that: 1 <= 3
1) I know that 1 <= 1 from (le_refl 1)
2) also I can understand substitution, so
I have 1 <= 2 from le_step : forall n m. n <= m ==> n <= m + 1 and le_refl : 1 <= 1

Backward proof:
Backward proof usually we get if we use tactic apply.
Backward proof is like answer to question:
What step must finishing this whole proof?
What we must apply to finish this proof? (1 step before)

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Sun 15 Aug 2021 16:36:16 No.13522441 Report

Quoted By:

Who are sheels?

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Sun 15 Aug 2021 16:38:48 No.13522447 Report

Quoted By:

What do you do? What kind of research?

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Sun 15 Aug 2021 16:52:52 No.13522490 Report

Quoted By: >>13522717

If anyone interested in learning such software, or making it better, I can help.

Anonymous

Anonymous Sun 15 Aug 2021 18:26:46 No.13522717 Report

Quoted By: >>13522883

>>13522490
Do you have a source on how to learn a simple proof?
I always wanted to make a simple proof of the irrationality of sqrt(2), but given how simple the proof is, I can't make one work in these programs and it annoys me because they're supposed to make things easier, not harder.

Anonymous

Anonymous Sun 15 Aug 2021 19:40:19 No.13522883 Report

Quoted By: >>13522890 >>13524742 >>13525878

>>13522717

No you don't get the point.
The point is that, is you translate a proof in Coq, it will tell you within a second if it's right or wrong and if wrong, where it is.

You input a 100 pages masterpiece and Coq tells you that at the page 79 you misused $H^{\frac{1}{2} }_0$ for $H^1_0$ , you do not need the help of the whole mathematician community for that.

Anonymous

Anonymous Sun 15 Aug 2021 19:41:58 No.13522890 Report

Quoted By: >>13522910 >>13523590

>>13522883
Yeah but why would I want to input a complicated proof into that shit when I can't even input a simple one?

Why would I want to work with something that promises to make our work irrelevant?

I would if the interface was less shit.

Anonymous

Anonymous Sun 15 Aug 2021 19:48:33 No.13522910 Report

Quoted By: >>13526036

>>13522890

I think it's because it's developed by a team of 4 people. ^^'
They mainly lack of manpower for this.

Anonymous

Anonymous Sun 15 Aug 2021 22:54:17 No.13523482 Report

Quoted By:

Keep bumping, OP, the topic sounds rather interesting

Anonymous

Anonymous Sun 15 Aug 2021 23:24:10 No.13523590 Report

Quoted By: >>13524122 >>13524614 >>13526024

>>13522890

> Why would I want to work with something that promises to make our work irrelevant?

For one, anyone who has used these things knows that promise is a never going to be realized because automating mathematical proving is equivalent to solving the halting problem.

Second, here's a point that pseuds on /sci/ will not tell you: often times when a theorem gets formalized on a computer, what happens is that it forces the author to think very deeply about the theorem and come up with an entirely different proof, revealing some new insight in the process. Proof assistants force you to be 100% rigorous, and this usually reveals millions of minor problems that would have been basically glossed over in a trad "pen and paper" proof.

Another important advantage of proof assistants is that it could be argued that the mathematical foundations that proof assistants are based on renders set theory obsolete. Think about it: the reason why we don't have any set theory-based proof assistants is precisely because of my point in the previous paragraph. When you try to input set theory into a computer, it uncovers bajillions of problems. This is actually a perfect example: the process of inputting set theory into the computer uncovered 1000 trillion different problems that the inventors of set theory never considered, and this led to a whole plethora of new insights and founded an entire sub-field.

Anonymous

Anonymous Sun 15 Aug 2021 23:34:53 No.13523623 Report

Quoted By: >>13523633

>>13522412
What's hard math for you?

Anonymous

Anonymous Sun 15 Aug 2021 23:38:13 No.13523633 Report

Quoted By:

>>13523623
Trig identities.

Anonymous

Anonymous Sun 15 Aug 2021 23:45:57 No.13523662 Report

Quoted By:

>>13522412
>implying 2ch brainlet subhumans know any serious math
kek

Anonymous

Anonymous Mon 16 Aug 2021 02:58:42 No.13524122 Report

Quoted By: >>13525223

>>13523590
Where can I read more about this subject, anon?

Anonymous

Anonymous Mon 16 Aug 2021 06:31:09 No.13524614 Report

Quoted By:

>>13523590
Godspeed, anon! Looking forward to read more post by you.

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Mon 16 Aug 2021 07:54:50 No.13524742 Report

Quoted By: >>13525575 >>13530381

>>13522883
Firstly, learn about lambda calculus. (~1 hour)
www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf

Secondly, learn about Lean theorem prover (~2 hours)
1. Hitchhiker’s guide to Logic Verification — for Computer Scientists
2. Natural number game

Some useful links
https://wiki.alcidesfonseca.com/lean-theorem-prover/

Then you ready to learn about Coq. (~? hours)
+ Install Coq.
* variant-1 use online jsCoq
Link: https://x80.org/collacoq/

* variant-2 install Coq on your machine.
Link: https://github.com/coq/platform/releases/tag/2021.02.1

+ See some tutorials and motivating videos.
1. Formal Methods for the Informal Engineer: Tutorial #2 - The Coq Theorem Prover (2021)

https://youtu.be/5e7UdWzITyQ?t=1876

File used in tutorial:
https://raw.githubusercontent.com/codyroux/broad-coq-tutorial/master/tutorial.v

2. How to use CoqIDE
https://www.youtube.com/watch?v=7sk8hPWAMSw

3. Introductory Proof: Commutativity of Addition in Coq
https://www.youtube.com/watch?v=OaIn7g8BAIc

4. Dr Thorsten Altenkirch discusses Type Theory vs Set Theory.
https://www.youtube.com/watch?v=qT8NyyRgLDQ

5. George Hotz | Programming | The Coq Files: sqrt(2) is irrational | Part1
https://youtu.be/bTLc_9buWLQ?t=585

+ Wait my instructions (I have proof that 2 is irrational, but I need to correct some errors)
or do it yourself :)

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Mon 16 Aug 2021 09:47:45 No.13524900 Report

Quoted By:

"necessarily incomplete tutorial" by Yale University
https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf

Anonymous

Anonymous Mon 16 Aug 2021 12:30:21 No.13525223 Report

Quoted By:

>>13524122

the book "homotopy type theory" is pretty decent

Anonymous

Anonymous Mon 16 Aug 2021 14:34:20 No.13525508 Report

Quoted By:

>>13522384
These systems most certainly have a place in mathematics, as evidenced by e.g. the proof of the Four color theorem and the Kepler conjecture. Most people, I assume, are apathetic to them because they aren't capable of automatically producing novel proofs (which might not be the case for very long, thanks to advances in machine learning). With regards to learning, I don't think it's much different than with any other programming language. I recommend reading through Lean's mathlib and seeing how they define certain objects and how they go about proving things with them. There's also the Software Foundations series, which is good if you're a complete beginner to formalization.

Anonymous

Anonymous Mon 16 Aug 2021 14:59:50 No.13525575 Report

Quoted By:

>>13524742
Why should you use coq instead of just lean?

Anonymous

Anonymous Mon 16 Aug 2021 15:02:35 No.13525582 Report

Quoted By: >>13525625

>>13522384
use python you unbelievable moron

Anonymous

Anonymous Mon 16 Aug 2021 15:16:39 No.13525625 Report

Quoted By: >>13525936

>>13525582
It's so Basic.

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Mon 16 Aug 2021 16:19:25 No.13525829 Report

Quoted By:

Theoretically if you have super-mega-computer you can prove not all, but big number of mini-

theorems. This can be helpful if you want to semi-automate writing libraries (big set of mini

facts) to Lean or Coq.
But it is worth noting that unfortunately there is no way (using only assistents) to

calculate/plan the properties of proofs.

if you think of a proof as a path in a graph, then if the path can have some interesting

properties, such as the number of loops, the number of vertices that are different to some f

(node), then the proof can also have properties.

The ability of making plan for proof can be useful when creating long proofs.

For example:
start -> node2 -> node3 -> ... -> finish
node2 must use lemmas from Nat library
But node3 use only two or less from setB
Whole proof don't use complex number at all...
...
Coq, please check that proof A is a shortest.
Coq: NO.
Please calculate for me shortest proof.
Coq logged to console: (t1 t2 (t3 t4 a b c) (t5 _ _ d x y)) ... )()( ...
[length of message = 999999]
Stop, that proof is minimal?
Please, give me proof that THIS PROOF is minimal.
Ok, Sir: (T1 T2 T3 ...
[length of message = 999999999]
...[Human closed window]

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Mon 16 Aug 2021 16:22:32 No.13525840 Report

Quoted By:

The solution to the problem can be difficult and simple at the same time.
I'm thinking about minimizing the proof, not just whether it's true or false, but all the way,

all the way which is full of mathematical adventures.

The questions might sound like this:
1. How to define properties of proofs and in general, properties of meta (higher than proofs)

objects.
2. How to automate creating API's + type annotations + fill some wildcards "_" if possible?
3. How to implement backtracking in interactive mode:
Example:
begin
apply t1,
apply t2,
rw t3,
exact t4,
end

With backtracking feature, one could simply write:
begin
find_proof [max_depth := 4, set_of_theorems := [t1, t2, t3, t4]],
end

And that function prints to console list of valid tactic sequeces (list of lists).

Now in lean you can already use backtracking but only for special tactics:
1. Only for apply. "solve_by_elim"
2. Only for rewriting. "rewrite_search"
But what if you want to solve this:
begin
apply t1
rewrite t2,
end

I don't know way to solve this without rewriting lean code.

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Mon 16 Aug 2021 16:36:30 No.13525878 Report

Quoted By:

>>13522883
I have presentaion in google docs about Coq theorem prover.
Please notice if that link don't work.

https://docs.google.com/presentation/d/1HbhmoI7qFP2kgngEmc4KKCziCNctvQ4f5KB7GmLXo34/edit?usp=sharing

Mathematical proof? What is it actually?

Mathematical proof? What is it actually? Mon 16 Aug 2021 16:56:22 No.13525922 Report

Quoted By:

How to learn Coq?
1. Learn Lambda calculus carefully.
2. Read about propositions. (P -> Q) -> R stuff like that
3. Try to prove several simple facts with pan and paper. (Commutativy of addition, Associativity)
4. Learn Inductive types. (Enums, Lists, Trees)
5. Learn about "How to write proof in one line".
Bonus we can define sorry like in lean:
Axiom sorry : forall {A : Type}, A.
And use it:
Example add_0_r : forall n : nat, n + 0 = n := sorry.
But it's only for leaning not for serious projects, because we need to highlight sorry keyword, like highlighted `Admitted`.
6. Try learn about well-founded things (recursion, induction).
7. Sqrt(2) is irrational? really?
8. Read in docs about Ltac2 language.
9. Write your own tactics.

This list can be changed. I don't think that's enough to study a topic like this.

Anonymous

Anonymous Mon 16 Aug 2021 17:02:08 No.13525936 Report

Quoted By:

>>13525625
you can do whatever you want include basic things, I do not understand what you're trying to say here

Anonymous

View Same Google iqdb SauceNAO 1612027575132.jpg, 92KiB, 750x1000

Anonymous Mon 16 Aug 2021 17:30:33 No.13526024 Report

Quoted By:

>>13523590
>When you try to input set theory into a computer, it uncovers bajillions of problems.

Yes and no. It's not so much that you face foundational problems, but rather that ZF is very ill-fitted for human use.

It's as if you were writing code in assembly, i.e. in theory you can write everything with it but in practice it's a horrible unmaintainable mess that requires a lot of work to get anything done the wrong way. Type theory is a bit better in this respect because it aligns quite well with daily mathematical practice, but there are still a hell of a lot of pain points. Mechanizing a proof takes several orders of magnitude more work than paper handwaving. So we're not quite there yet.

> t. expert in type theory and proof assistants

Anonymous

Anonymous Mon 16 Aug 2021 17:34:04 No.13526036 Report

Quoted By: >>13526165

>>13522910
Nope, there are more than 4 Coq developers out there. The issue is that they're all PLT nerds who are utterly unable to write a fucking user interface.

Also, you should try the vscoq plugin for vscode rather than the antiquated CoqIDE interface.

Anonymous

Anonymous Mon 16 Aug 2021 18:23:46 No.13526165 Report

Quoted By: >>13526260

>>13526036

proof general for emacs is the optimal set-up. Microshaft VS Code is a steaming pile of dog shit.

> Boohoo nerds can't make a good UI!!!!

No, you just never read the Emacs manual (i.e., you're incompetent.) Proof general can be configured to work however you want it to work. This is how I configured it:

;; In Proof General:
;; - Bind F1 to "Next"
;; - Bind F2 to "Undo"
;; - Bind F3 to "Goto"
;; - Bind F4 to execute C-c C-l, which sets up the 3 window hybrid format.
(defun setup-proof-general ()
(global-set-key [f1] (quote proof-assert-next-command-interactive))
(global-set-key [f2] (quote proof-undo-last-successful-command))
(global-set-key [f3] (quote proof-goto-point))
(global-set-key [f4] (quote "\C-c\C-l"))
)
(add-hook 'coq-mode-hook 'setup-proof-general)

Anonymous

View Same Google iqdb SauceNAO MV5BYWVlYjBk.jpg, 87KiB, 458x755

Anonymous Mon 16 Aug 2021 18:57:05 No.13526260 Report

Quoted By:

>>13526165
>proof general
Literal pile of shit written with ELISP regexps. Your opinion is dismissed.

Anonymous

Anonymous Tue 17 Aug 2021 11:07:42 No.13528341 Report

Quoted By:

>bumps

Anonymous

Anonymous Tue 17 Aug 2021 18:20:39 No.13529603 Report

Quoted By:

rebumped

Anonymous

Anonymous Tue 17 Aug 2021 21:38:16 No.13530381 Report

Quoted By: >>13530698

>>13524742
Thank you, I wanted to learn this stuff some time ago but couldn't find good material to do that.

Anonymous

Anonymous Tue 17 Aug 2021 23:09:25 No.13530698 Report

Quoted By:

>>13530381
Interested in doing that together? Nothing binding

Anonymous

Anonymous Wed 18 Aug 2021 00:31:54 No.13530966 Report

Quoted By:

>>13522384
An interesting thread for a change.

Anonymous

Anonymous Wed 18 Aug 2021 10:01:13 No.13531957 Report

Quoted By:

Anonymous

Anonymous Wed 18 Aug 2021 17:36:32 No.13533122 Report

Quoted By:

Anonymous

Anonymous Wed 18 Aug 2021 18:23:54 No.13533304 Report

Quoted By: >>13533789

>>13522384
I know Haskell, that code looks a lot like Haskell
I can somehow read that code

Anonymous

Anonymous Wed 18 Aug 2021 20:49:07 No.13533789 Report

Quoted By: >>13535851

>>13533304

> he knows haskell

you must have an IQ above 3000

Anonymous

Anonymous Thu 19 Aug 2021 12:05:53 No.13535851 Report

Quoted By:

>>13533789
Is it that hard?

Anonymous

Anonymous Thu 19 Aug 2021 22:26:31 No.13537805 Report

Quoted By:

Capcode	All Only User Posts Only Moderator Posts Only Admin Posts Only Developer Posts
Show Posts	All Only With Images Only Without Images
Deleted Posts	All Only Deleted Posts Only Non-Deleted Posts
Ghost Posts	All Only Ghost Posts Only Non-Ghost Posts
Post Type	All Only Sticky Threads Only Opening Posts Only Reply Posts
Results	All Grouped By Threads
Order	Latest Posts First Oldest Posts First

Your latest searches