Proof Assistants Beta
TheGhostOfGaussPossessesMe's user avatar
TheGhostOfGaussPossessesMe's user avatar
TheGhostOfGaussPossessesMe's user avatar
TheGhostOfGaussPossessesMe
  • Member for 1 year, 7 months
  • Last seen more than a month ago
Profile Activity
Stats
267
reputation
1k
reached
1
answer
7
questions
Communities
View all
About

Amateur mathematician. Software developer.

“[Mathematics is] only real when shared” ― Jon Krakauer, Into the Wild

My new favorite book:

Theories, Sites, Toposes; by Olivia Caramello

It is unbelievably readable for modern graduate students or those familiar with basic Category Theory. This is in contrast to the difficulty one has when they start up Johnstone's books. Olivia Caramello is a super hero of mathematics.

Badges
This user doesn’t have any gold badges yet.
1
silver badge
8
bronze badges
Top tags
View all tags
2
Score
3
Posts
38
Posts %
0
Score
5
Posts
62
Posts %
0
Score
3
Posts
38
Posts %
0
Score
2
Posts
25
Posts %
0
Score
2
Posts
25
Posts %
0
Score
2
Posts
25
Posts %
Top posts
All Questions Answers
Score Newest
question
4
How can you represent a dependent type visually?
Nov 3, 2022
question
3
Do implementations of a PA and of ATP have overlap?
Oct 30, 2022
answer
2
How to implement a visual proof assistant?
Oct 3, 2022
question
1
Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?
May 23
question
1
Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?
Aug 28, 2022
question
1
How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?
Oct 10, 2022
question
0
How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?
Oct 26, 2022
question
-3
Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?
Oct 3, 2022
Top network posts
View all network posts
64
Is it not effective to learn math top-down?
45
What is integration by parts, really?
41
Under the Curry-Howard correspondence or loosely "proofs-as-programs", do we also have "programs-as-proofs" and what would some arb. program prove?
28
Group formed on Parabola similarly to how an Elliptic curve forms a group (by drawing lines, circles, intersecting, or taking tangent lines)
24
Every natural number is covered by consecutive numbers that sum to a prime power.

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.