satnam6502

Using a Reasonging LLM to find Agda proofs of theorems

As a wee experiment, I've produced a simple Haskell program that sends a prompt containing a lemma to prove in Agda to an LLM. The program checks the LLM-generated proof by invoking Agda, and if the proof contains an error then this is fed back to the LLM and it is asked to try again. This process repeats until a proof passes, or the user aborts (or the LLM reaches some rate limit). The LLMs that I tested were the basic (non-reasoning) models from Claude (e.g. Sonnet 3.7), Llama3 and Llama 4 variants, a version of DeepSeek, a version of Qwen 32B, and the o3 reasoning model from ChatGPT (plus a few others). The experiment here has no human in the loop, the LLM has to produce a totally syntactically correct Agda program which needs to be typed-checked by Agda without any interactive editing or "fix up". The goal here is not to produce a nice proof like one a human might write, but instead to

satnam6502

package main

import (
	"fmt"
	"io/ioutil"
	"log"
	"path/filepath"
	"strings"

	"github.com/lunny/axmlParser"

satnam6502

I0321 21:34:20.603305   22897 serve_hostnames.go:53] Starting serve_hostnames soak test with queries=10000 and perNode=30 upTo=100
I0321 21:34:21.217231   22897 serve_hostnames.go:78] Nodes found on this cluster:
I0321 21:34:21.217270   22897 serve_hostnames.go:80] 0: kubernetes-minion-08vl.c.kubernetes-scale.internal
I0321 21:34:21.217276   22897 serve_hostnames.go:80] 1: kubernetes-minion-14sw.c.kubernetes-scale.internal
I0321 21:34:21.217280   22897 serve_hostnames.go:80] 2: kubernetes-minion-16y7.c.kubernetes-scale.internal
I0321 21:34:21.217284   22897 serve_hostnames.go:80] 3: kubernetes-minion-1xeu.c.kubernetes-scale.internal
I0321 21:34:21.217287   22897 serve_hostnames.go:80] 4: kubernetes-minion-2y1m.c.kubernetes-scale.internal
I0321 21:34:21.217291   22897 serve_hostnames.go:80] 5: kubernetes-minion-37uc.c.kubernetes-scale.internal
I0321 21:34:21.217295   22897 serve_hostnames.go:80] 6: kubernetes-minion-3gif.c.kubernetes-scale.internal
I0321 21:34:21.217298   22897 serve_hostnames.go:80] 7: kubern

satnam6502

satnam@satnam-linux:~/kubernetes$ cluster/kubectl.sh get replicationControllers
Running: cluster/../cluster/gce/../../platforms/linux/amd64/kubectl get replicationControllers
CONTROLLER                           CONTAINER(S)            IMAGE(S)                            SELECTOR                     REPLICAS
elasticsearch-logging-controller     elasticsearch-logging   dockerfile/elasticsearch            name=elasticsearch-logging   1
kibana-logging-controller            kibana-logging          kubernetes/kibana:1.0               name=kibana-logging          1
monitoring-heapsterController        heapster                kubernetes/heapster:v0.6            name=heapster                1
monitoring-influxGrafanaController   influxdb                kubernetes/heapster_influxdb:v0.3   name=influxGrafana           1
                                     grafana                 kubernetes/heapster_grafana:v0.3                                 
skydns                               etcd                    quay.io/coreos

satnam6502

satnam@satnam:~/gocode/src/github.com/GoogleCloudPlatform/kubernetes$ cluster/kube-down.sh 
Bringing down cluster using provider: gce
Project: kubernetes-satnam (autodetected from gcloud config)
Project: kubernetes-satnam (autodetected from gcloud config)
Bringing down cluster
INFO: Enabling auto-delete on kubernetes-master (kubernetes-master).
INFO: Waiting for delete of route kubernetes-minion-4. Sleeping for 3s.
INFO: Waiting for delete of firewall kubernetes-master-https. Sleeping for 3s.
INFO: Waiting for delete of route kubernetes-minion-10. Sleeping for 3s.
INFO: Waiting for delete of route kubernetes-minion-3. Sleeping for 3s.

satnam6502

Table of operations:

+---------------------------------------------------------+--------+-------------------------------+----------------+
| name                                                    | status | insert-time                   | operation-type |
+---------------------------------------------------------+--------+-------------------------------+----------------+
| operation-1416440235899-5083eb11b3879-961e8f1c-0913f3fc | DONE   | 2014-11-19T15:37:16.008-08:00 | insert         |
+---------------------------------------------------------+--------+-------------------------------+----------------+
Error: Internal Error
INFO: Waiting for insert of instance kubernetes-master. Sleeping for 3s.
INFO: Waiting for insert of instance kubernetes-minion-3. Sleeping for 3s.

satnam6502

satnam@satnam:~/gocode/src/github.com/GoogleCloudPlatform/kubernetes$ vagrant up
Bringing machine 'master' up with 'virtualbox' provider...
Bringing machine 'minion-1' up with 'virtualbox' provider...
Bringing machine 'minion-2' up with 'virtualbox' provider...
Bringing machine 'minion-3' up with 'virtualbox' provider...
==> master: Box 'fedora20' could not be found. Attempting to find and install...
    master: Box Provider: virtualbox
    master: Box Version: >= 0
==> master: Adding box 'fedora20' (v0) for provider: virtualbox
    master: Downloading: http://opscode-vm-bento.s3.amazonaws.com/vagrant/virtualbox/opscode_fedora-20_chef-provisionerless.box

satnam6502

The user name and password to use is located in ~/.kubernetes_auth.

F1108 12:47:50.147871 12630 kubecfg.go:436] Failed to print: template: output:1:7: executing "output" at <.items>: items is not a field of struct type *api.MinionList
Raw received object:
&api.MinionList{TypeMeta:api.TypeMeta{Kind:"", APIVersion:""}, ListMeta:api.ListMeta{SelfLink:"/api/v1beta1/minions", ResourceVersion:""}, Items:[]api.Minion{api.Minion{TypeMeta:api.TypeMeta{Kind:"", APIVersion:""}, ObjectMeta:api.ObjectMeta{Name:"kubernetes-minion-1.c.kubernetes-elk.internal", Namespace:"", SelfLink:"/api/v1beta1/minions/kubernetes-minion-1.c.kubernetes-elk.internal", UID:"", ResourceVersion:"7", CreationTimestamp:util.Time{Time:time.Time{sec:63551076437, nsec:0x0, loc:(*time.Location)(0xa98e80)}}, Labels:map[string]string(nil), Annotations:map[string]string(nil)}, HostIP:"", NodeResources:api.NodeResources{Capacity:api.ResourceList{"memory":util.IntOrString{Kind:0, IntVal:4026531840, StrVal:""}, "cpu":util.IntOrString{Kind:0, IntVal:1000,

satnam6502

$ cluster/kube-up.sh
Starting cluster using provider: gce
... calling verify-prereqs
... calling kube-up
Project: kubernetes-satnam2
Zone: us-central1-b
+++ Staging server tars to Google Storage: gs://kubernetes-staging-a2dc4/devel
current-context: "kubernetes-satnam2_kubernetes"
Running: cluster/../cluster/gce/../../cluster/../cluster/gce/../../_output/dockerized/bin/darwin/amd64/kubectl config view -o template --template={{$dot := .}}{{with $ctx := index $dot "current-context"}}{{$user := index $dot "contexts" $ctx "user"}}{{index $dot "users" $user "auth-path"}}{{end}}
Starting VMs and configuring firewalls

satnam6502

bash-3.2$ boot2docker stop
bash-3.2$ boot2docker download
Latest release for boot2docker/boot2docker is v1.3.1
Downloading boot2docker ISO image...
Success: downloaded https://github.com/boot2docker/boot2docker/releases/download/v1.3.1/boot2docker.iso
	to /Users/satnam/.boot2docker/boot2docker.iso
bash-3.2$ boot2docker start
Waiting for VM and Docker daemon to start...
...................oo
Started.