Groups
Sign in
Groups
Ghilbert
Conversations
About
Send feedback
Help
Ghilbert
Contact owners and managers
1–30 of 68
Mark all as read
Report group
0 selected
Adam Bliss
,
Mario Carneiro
3
4/20/19
Substitution operator on non-wff tvars
I will return to this topic in more depth later, but for now I will point you to my project metamath
unread,
Substitution operator on non-wff tvars
I will return to this topic in more depth later, but for now I will point you to my project metamath
4/20/19
Adam Bliss
, …
Raph Levien
5
3/31/19
Re: Ghilbert stuff
Norm, Raph, thanks for the replies. One of the main things I'm still confused about is whether my
unread,
Re: Ghilbert stuff
Norm, Raph, thanks for the replies. One of the main things I'm still confused about is whether my
3/31/19
Sidharth Ghoshal
, …
Adam Bliss
4
12/9/18
Understanding where implicit assumptions enter Euclid's Proof.
It may also be worth noting that the important operations on Tuples, such as indexing, are defined
unread,
Understanding where implicit assumptions enter Euclid's Proof.
It may also be worth noting that the important operations on Tuples, such as indexing, are defined
12/9/18
Sidharth Ghoshal
,
Raph Levien
2
12/9/18
Is this project still alive?
It's pretty much on hold. Raph On Sat, Dec 8, 2018 at 9:28 PM 'Sidharth Ghoshal' via
unread,
Is this project still alive?
It's pretty much on hold. Raph On Sat, Dec 8, 2018 at 9:28 PM 'Sidharth Ghoshal' via
12/9/18
Raph Levien
, …
Jim Kingdon
4
9/14/17
Progress: HTML theorem display with interactivity
With respect to intuitionistic logic, I trust people have seen http://wikiproofs.org/w/index.php?
unread,
Progress: HTML theorem display with interactivity
With respect to intuitionistic logic, I trust people have seen http://wikiproofs.org/w/index.php?
9/14/17
Raph Levien
3
9/11/17
A theory interpretation
To close the loop on this a bit, I thought for a while about how my original idea might be fixable,
unread,
A theory interpretation
To close the loop on this a bit, I thought for a while about how my original idea might be fixable,
9/11/17
Raph Levien
8/23/17
Progress: first translations from set.mm into new Ghilbert
One of the mistakes I feel I made in the previous prototype was not putting enough emphasis into
unread,
Progress: first translations from set.mm into new Ghilbert
One of the mistakes I feel I made in the previous prototype was not putting enough emphasis into
8/23/17
Raph Levien
7/22/17
Rough proposal for types and modules
I've been thinking a lot, and think I have a rough design including simple types, and also
unread,
Rough proposal for types and modules
I've been thinking a lot, and think I have a rough design including simple types, and also
7/22/17
Raph Levien
,
Adam Bliss
3
7/13/17
LF (lambda-pi) explorations
Quick notes, I'm still wrapping my head around some of these questions. My intuition is that
unread,
LF (lambda-pi) explorations
Quick notes, I'm still wrapping my head around some of these questions. My intuition is that
7/13/17
Raph Levien
7/3/17
Progress: infix syntax, definitions
A lot of progress, including infix syntax (using a precedence parser) and definitions. The prototype
unread,
Progress: infix syntax, definitions
A lot of progress, including infix syntax (using a precedence parser) and definitions. The prototype
7/3/17
Raph Levien
6/24/17
Progress: bound variables
As of the latest commit, the Rust prototype now handles bound variables (with lambda syntax) and
unread,
Progress: bound variables
As of the latest commit, the Rust prototype now handles bound variables (with lambda syntax) and
6/24/17
Raph Levien
, …
Norman Megill
10
6/21/17
Progress: unification based checking in the new syntax
On Wednesday, June 21, 2017 at 9:18:29 AM UTC-4, Raph wrote: That's very interesting, and further
unread,
Progress: unification based checking in the new syntax
On Wednesday, June 21, 2017 at 9:18:29 AM UTC-4, Raph wrote: That's very interesting, and further
6/21/17
Adam Bliss
,
Raph Levien
8
6/11/17
Updates?
Thanks Raph. I found the LF paper to be a bit dense. But after working through chapters 1 and 2 of
unread,
Updates?
Thanks Raph. I found the LF paper to be a bit dense. But after working through chapters 1 and 2 of
6/11/17
Paul Merrell
, …
Raph Levien
6
6/5/17
Website Issues
This should be fixed. Thanks to both of you for noticing and fixing. I also updated the github repo
unread,
Website Issues
This should be fixed. Thanks to both of you for noticing and fixing. I also updated the github repo
6/5/17
Raph Levien
,
Adam Bliss
3
6/4/17
Ghilbert 2 sketch
Both are typos. I originally had {} instead of ::() but realized it would be impossible to
unread,
Ghilbert 2 sketch
Both are typos. I originally had {} instead of ::() but realized it would be impossible to
6/4/17
Marnix Klooster
, …
Steven Baldasty
7
9/30/15
Ghilbert/Metamath proof repository ideas
I read a paper about the theory of General Logics recently. If memory serves, the properties of
unread,
Ghilbert/Metamath proof repository ideas
I read a paper about the theory of General Logics recently. If memory serves, the properties of
9/30/15
Marnix Klooster
,
Carl Witty
2
2/3/15
Expressive power of 'def' vs. 'defthm'?
On Fri, Jan 30, 2015 at 9:36 AM, Marnix Klooster <marnix....@gmail.com> wrote: > Hello
unread,
Expressive power of 'def' vs. 'defthm'?
On Fri, Jan 30, 2015 at 9:36 AM, Marnix Klooster <marnix....@gmail.com> wrote: > Hello
2/3/15
Robert Solovay
,
Adam Bliss
2
11/15/14
Invite codes
Hi Dr. Solovay, I'm excited to hear that you're interested in Ghilbert! You can use the
unread,
Invite codes
Hi Dr. Solovay, I'm excited to hear that you're interested in Ghilbert! You can use the
11/15/14
Robert Solovay
11/15/14
Invite codes
I've got an invite coe from Raph but I'm not sure where and how its used/ Also is there some
unread,
Invite codes
I've got an invite coe from Raph but I'm not sure where and how its used/ Also is there some
11/15/14
Jim Kingdon
, …
Adam Bliss
10
10/30/14
(probable) bugs in javascript verifier
Hey, all that work looks awesome! Love all the new tests, and I learned about istanbul-js (which I
unread,
(probable) bugs in javascript verifier
Hey, all that work looks awesome! Love all the new tests, and I learned about istanbul-js (which I
10/30/14
Bruno Schiavo
,
Paul Merrell
2
10/11/14
New member
Welcome, Bruno! Can you create an account through this link: https://ghilbert-app.appspot.com/account
unread,
New member
Welcome, Bruno! Can you create an account through this link: https://ghilbert-app.appspot.com/account
10/11/14
Joe Corneli
9/20/14
compiling from hcode to ghilbert
Hi all: Some years ago Raph and I had a few exchanges on the AsteroidMeta wiki about "hcode
unread,
compiling from hcode to ghilbert
Hi all: Some years ago Raph and I had a few exchanges on the AsteroidMeta wiki about "hcode
9/20/14
Raph Levien
, …
fl
13
5/5/14
Step theorem display and HTML typesetting
I'm a big fan of Dijkstra's calculational proofs The problem is not calculational proofs (
unread,
Step theorem display and HTML typesetting
I'm a big fan of Dijkstra's calculational proofs The problem is not calculational proofs (
5/5/14
Cris Perdue
,
Raph Levien
2
4/10/14
Expressing free variables in the metalogic
Hi and welcome to Ghilbert! As you mentioned in another thread while this message was stuck in
unread,
Expressing free variables in the metalogic
Hi and welcome to Ghilbert! As you mentioned in another thread while this message was stuck in
4/10/14
Paul Merrell
, …
Jim Kingdon
13
3/30/14
Technical Difficulties
Good summary of the issue, Raph. I'm not sure how many words to attempt on "people who
unread,
Technical Difficulties
Good summary of the issue, Raph. I'm not sure how many words to attempt on "people who
3/30/14
Paul Merrell
3/5/14
LaTex Typesetting
I am pleased to announce that we now have proper typesetting integrated into Ghilbert. I'm sure
unread,
LaTex Typesetting
I am pleased to announce that we now have proper typesetting integrated into Ghilbert. I'm sure
3/5/14
Paul Merrell
,
Jim Kingdon
8
2/20/14
Reorganized Peano Directory
MathML might be a bit more natural, as I have read that it is more logical and LaTeX is more
unread,
Reorganized Peano Directory
MathML might be a bit more natural, as I have read that it is more logical and LaTeX is more
2/20/14
Paul Merrell
,
Jim Kingdon
3
1/3/14
Integers and Rationals
I finally got rational numbers working plus a bunch of other stuff I checked in over the break. I
unread,
Integers and Rationals
I finally got rational numbers working plus a bunch of other stuff I checked in over the break. I
1/3/14
Paul Merrell
, …
Jim Kingdon
6
12/21/13
Problem with the Python verifier
Excellent! Thanks for fixing that. On 12/19/2013 10:20 PM, Adam Bliss wrote: Thanks for the report (
unread,
Problem with the Python verifier
Excellent! Thanks for fixing that. On 12/19/2013 10:20 PM, Adam Bliss wrote: Thanks for the report (
12/21/13
Adam Bliss
12/15/13
Caghni update
On Nov 1, 2013 4:07 PM, "Adam Bliss" <abl...@gmail.com> wrote: > My hope is to
unread,
Caghni update
On Nov 1, 2013 4:07 PM, "Adam Bliss" <abl...@gmail.com> wrote: > My hope is to
12/15/13