Mastodawn

@dimpase
One can imagine that LLMs will eventually generate proofs that for computational burden reasons are uncheckable in practice.

What will it mean if the LLMs did what they normally did, and say this is a valid proof, but in practice no human+computer is currently or soon going to be able to check.

Alllsooo, if the formal logic is computer generated anyway, wouldn't a first order logic fully automatic theorem prover proof be infinitely better and equally easy i.e. #acl2 as #lean?
@tao

Show thread

screwlisp May 5

@kentpitman @prahou @davidrevoy @bagder @chiply @yantar92 @jackdaniel

I ran out of letters.
@mdhughes #coffee https://gamerplus.org/@mdhughes@appdot.net/116520397627957512

Some notes on my #lisp #hextille viz my https://lispy-gopher-show.itch.io/dl-roc-lisp apropos jd's #ecl and #McCLIM (clim 2 spec)
Same code:
- #fol #acl2
- #commonLisp (portable)
- #McCLIM -rich interface common lisp
- Inside C programs
- Inside C++ programs
- Inside WASM
- Curl inside it

Requests for questions/comments to pass on to the tagged project authors too please.

Digital Mark λ ☕️ 🌮 🚀 🌗 (@[email protected])

OK, I think we're good now. https://cyberhole.online/coffee.html

AppDot.Net

screwlisp May 5

#lispyGopherClimate

https://toobnix.org/w/mu2Wm3Y7F6dBbqBivkXL1x

#climateCrisis #poem @kentpitman
- Comments on responsible dialog, many notes
@prahou and @davidrevoy 's #exquisiteCorpse #art #unix_surrealism https://gamerplus.org/@screwlisp/116518727790621795

/Next Sunday/Tuesday/Sunday/ upcoming guests: @bagder #curl @chiply #emacs @yantar92 #orgMode

#lisp / #commonLisp / #acl2 since I did not finish, my #commonLisp *my* #hextille wishlist https://lispy-gopher-show.itch.io/dl-roc-lisp/devlog/1502166/six-dimensional-hextille-boondoggle-acl2-mcclim-common-lisp before @jackdaniel 's coming #ELS #ecl #McCLIM thing.

#lambdaMOO !

screwlisp Apr 28

#Boondoggle of sixdimensional proportions. I don't know about you, but if I so much as look at the attached #hextille I lose my balance.

https://lispy-gopher-show.itch.io/dl-roc-lisp/devlog/1502166/six-dimensional-hextille-boondoggle-acl2-mcclim-common-lisp

I kind of finish a very handy and #acl2 #logic ally sound, and #McCLIM hextille.lisp - which I would be interested to see /you/ use in response, it should be easy as pie - but get lost in the weeds proposing a 3D + also 3 more D 6-hextille.lisp version. I could not get it out of my head, so we all must suffer.

#commonLisp #geometry

screwlisp Apr 27

More hexagon #acl2 #firstOrderLogic in one #ecl #commonLisp source with #McCLIM #graphics . Er.. #hextille .
https://lispy-gopher-show.itch.io/dl-roc-lisp/devlog/1500993/more-hexagon-acl2-first-order-logicembeddable-common-lispmcclim-graphics
I am quite excited to have same source*
*read the article
Generating automatic first order #logic theorems on the left, ANSI common lisp running on the right, and #CLIM graphics popped up in the foreground.

In practice, the article is a show-and-tell of the functions I wrote today. They are quite cautious, recursive and explicit as I get more used to the #fol atm

screwlisp Apr 24

Well, I have to say I am on painkillers these days, but I wrote this.

https://lispy-gopher-show.itch.io/dl-roc-lisp/devlog/1497995/hexagons-common-lisp-interface-manager-graphics-and-acl2-first-order-logic-automatic-proofs-in-one-place

#McCLIM #acl2 #commonLisp #programming #logic #graphics #hextille

sharpsign logically drawing hexagons.

Edit: It's about a single lisp source spanning both common lisp interface manager and acl2 first order logic.

Show thread

screwlisp Apr 6

Addendum Summarizing / lining up the #commonLisp #conditionSystem version with the #acl2 #logic version:

https://lispy-gopher-show.itch.io/lispmoo2/devlog/1481671/summary-how-common-lisp-conditions-line-up-to-the-acl2-theorem-accidental-common-lisp-metaobject-protocol-eg

Also an unintended #mop #demo

Summary how common lisp conditions line up to the acl2 theorem + accidental common lisp metaobject protocol e.g. - lispmoo2 by screwtape

We should do the ansi common lisp side of the acl2 first order logic condition theorem. (define-condition awkward () ((keys :initarg :keys :reader keys))) Quick fix: mop the keys to be the ones your c...

itch.io

screwlisp Apr 6

https://lispy-gopher-show.itch.io/lispmoo2/devlog/1481398/homespun-acl2-handler-bind-condition-handling

#acl2 simple introduction to acl2 for the #commonLisp inclined.

loop$, apply$, thms oh my.

In particular, I implement a model of a simple case of the common lisp condition system that is directly compatible with both ansi common lisp and acl2. (a computational logic for applicative common lisp).

#firstOrderLogic #theoremProving #programming #logic #example

Technically this is in support of my lisp / moo compatibility layer but I am not going to beleaguer the tag.

Homespun acl2 handler-bind condition handling - lispmoo2 by screwtape

Even though LambdaMOO’s MOO language is not obsessed with first order logic, in my common lisp condition system mooing I am obsessed with first order logic. To that end I have here initially impleme...

itch.io

screwlisp Apr 6

tbh I'm not sure why #acl2 doesn't have getf. Here is my "do-loop$" loopy one. #commonLisp

ACL2 !>(forgetf :a '(:c d :a b))
B

(defun forgetf (key plist)
(loop$ with pl of-type list = plist
do
(cond ((null pl) (return nil))
((equal key (car pl))
(return (cadr pl)))
(t (setq pl (cddr pl))))))

screwlisp Apr 5

#peertube #live Sunday Easter Morning in Europe https://toobnix.org/w/gXLXQqxf5MYg1NDF2Ua6oA #commonLisp #acl2 #lambdaMOO

Archive: https://toobnix.org/w/11NoAMWBnW3oVZLxCVRAYr