Skip to main content
Proof Assistants Beta
Daniel Donnelly's user avatar
Daniel Donnelly's user avatar
Daniel Donnelly's user avatar
Daniel Donnelly
  • Member for 2 years, 10 months
  • Last seen this week
Profile Activity
Stats
313
reputation
3k
reached
2
answers
10
questions
Communities
View all
About

Students should be paid to attend school.

Badges
This user doesn’t have any gold badges yet.
1
silver badge
8
bronze badges
Top tags
View all tags
2
Score
5
Posts
42
Posts %
0
Score
7
Posts
58
Posts %
0
Score
4
Posts
33
Posts %
0
Score
3
Posts
25
Posts %
0
Score
3
Posts
25
Posts %
0
Score
3
Posts
25
Posts %
Top posts
View all questions and answers
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
2
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
1
Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?
May 23, 2023
question
1
Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?
Jul 27
question
1
What is a simple example of transforming some Objects / Arrows in visual, categorical definition into actual Coq code. An MWE recipe that is
Jul 28
question
1
Terms are not types, but could I have Type be a subclass of Term in my OOP / C++ dependent type hierarchy?
Nov 14
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
Top network posts
View all network posts
66
Is it not effective to learn math top-down?
47
What is integration by parts, really?
45
Under the Curry-Howard correspondence or loosely "proofs-as-programs", do we also have "programs-as-proofs" and what would some arb. program prove?
30
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.