there are undergrads here who don't know Coq

> there are undergrads here who don't know Coq
> there are mathematicians who dont know Coq
> there are COMPUTER SCIENTISTS who dont know Coq

i prefer doing math

if autists want to double check my obviously correct proofs, go for it

Nice now prove the 4 color theorem

logicians gtfo

Thousands of math and cs students love coq if you catch my drift

Are there any lewds of proof general tan?

>someone else on Veeky Forums likes Coq
neat.jpg

memes aside, how do I use PG with isabelle?

What's coq?

Curious as well : as a french speaker, I don't think they refer to the animal though.

A theorem prover

you tell it

>(A and B) implies (B and A)

and it spits out a formal proof of it. This is a silly example, but in that case it's

[math] \lambda p. \ (\pi_2 p, \pi_1 p) \ : \ a\times b \to b \times a [/math]

haHA you're referring to the male genitalia!

a programming language where you can prove theorems about functions you write

It has a lot of theory behind it and does everything your brain can do when it comes to math.

Cool, seems useful

>and does everything your brain can do when it comes to math
you don't really believe that, do you?

It can express any math that's worthwhile at least

We have 3 types of opsin molecules in our eyes each detecting various wavelengths of light corresponding to R B & G. The fourth corresponds to rodopsin which measures darkness as it is sensitive to a much wider wavelength

There is more information in a human brain than can be extracted on all the hardware produced till this day combined

What no, the software you stupid faggot

Why the homophobia?

Actually you tell it the proof and it tells you "yup, that's a proof!"

Coq is kinda addictive but it's a pain in the ass whenever you want to prove serious stuff with it. Most fun stuff I did was the infinite Ramsey theorem.

What happens when you plug in 1 + 2 + 3 + ...

= -1/0.99999....

Coq is cool. Convincing it something is a proof requires you to really understand the problem because vanilla type theory is pretty heavy-handed. Can't wait for HoTT-Coq.