add openai with rye add

README.md

@@ -31,6 +31,13 @@ challenging LLMs to write dependently typed _and_ formally verified code
 - [ ] trawl aoc of the ones we have lean4 solutions for some nontriviality:
   - meaning a way to beat the dumb way on O()
 
+## Conceptually 3
+- ask llm to generate property tests for apps problems
+- subject corresponding apps solutions to those property tests
+- ask llm to generate sorry'd out lean theorems from property tests
+- output task: original task plus sorry'd out lean theorems.
+
 ## TODO
 - [ ] read dafny benchmark paper
 - [ ] read the APPS easies.
+- [ ] remember that we should show baselines from openai, anthropic, and deepseek

nb/pyproject.toml

@@ -8,6 +8,7 @@ authors = [
 dependencies = [
     "datasets>=2.21.0",
     "anthropic>=0.34.2",
+    "openai>=1.44.1",
 ]
 readme = "README.md"
 requires-python = ">= 3.8"

nb/requirements-dev.lock

@@ -25,6 +25,7 @@ anyio==4.4.0
     # via anthropic
     # via httpx
     # via jupyter-server
+    # via openai
 argon2-cffi==23.1.0
     # via jupyter-server
 argon2-cffi-bindings==21.2.0
@@ -73,6 +74,7 @@ dill==0.3.8
     # via multiprocess
 distro==1.9.0
     # via anthropic
+    # via openai
 executing==2.1.0
     # via stack-data
 fastjsonschema==2.20.0
@@ -95,6 +97,7 @@ httpcore==1.0.5
 httpx==0.27.2
     # via anthropic
     # via jupyterlab
+    # via openai
 huggingface-hub==0.24.6
     # via datasets
     # via tokenizers
@@ -128,6 +131,7 @@ jinja2==3.1.4
     # via nbconvert
 jiter==0.5.0
     # via anthropic
+    # via openai
 json5==0.9.25
     # via jupyterlab-server
 jsonpointer==3.0.0
@@ -212,6 +216,8 @@ numpy==2.1.1
     # via datasets
     # via pandas
     # via pyarrow
+openai==1.44.1
+    # via nb
 overrides==7.7.0
     # via jupyter-server
 packaging==24.1
@@ -257,6 +263,7 @@ pycparser==2.22
     # via cffi
 pydantic==2.9.1
     # via anthropic
+    # via openai
 pydantic-core==2.23.3
     # via pydantic
 pygments==2.18.0
@@ -311,6 +318,7 @@ sniffio==1.3.1
     # via anthropic
     # via anyio
     # via httpx
+    # via openai
 sortedcontainers==2.4.0
     # via hypothesis
 soupsieve==2.6
@@ -334,6 +342,7 @@ tornado==6.4.1
 tqdm==4.66.5
     # via datasets
     # via huggingface-hub
+    # via openai
 traitlets==5.14.3
     # via comm
     # via ipykernel
@@ -354,6 +363,7 @@ types-python-dateutil==2.9.0.20240906
 typing-extensions==4.12.2
     # via anthropic
     # via huggingface-hub
+    # via openai
     # via pydantic
     # via pydantic-core
 tzdata==2024.1

nb/requirements.lock

@@ -24,6 +24,7 @@ anthropic==0.34.2
 anyio==4.4.0
     # via anthropic
     # via httpx
+    # via openai
 attrs==24.2.0
     # via aiohttp
 certifi==2024.8.30
@@ -39,6 +40,7 @@ dill==0.3.8
     # via multiprocess
 distro==1.9.0
     # via anthropic
+    # via openai
 filelock==3.16.0
     # via datasets
     # via huggingface-hub
@@ -54,6 +56,7 @@ httpcore==1.0.5
     # via httpx
 httpx==0.27.2
     # via anthropic
+    # via openai
 huggingface-hub==0.24.6
     # via datasets
     # via tokenizers
@@ -64,6 +67,7 @@ idna==3.8
     # via yarl
 jiter==0.5.0
     # via anthropic
+    # via openai
 multidict==6.0.5
     # via aiohttp
     # via yarl
@@ -73,6 +77,8 @@ numpy==2.1.1
     # via datasets
     # via pandas
     # via pyarrow
+openai==1.44.1
+    # via nb
 packaging==24.1
     # via datasets
     # via huggingface-hub
@@ -82,6 +88,7 @@ pyarrow==17.0.0
     # via datasets
 pydantic==2.9.1
     # via anthropic
+    # via openai
 pydantic-core==2.23.3
     # via pydantic
 python-dateutil==2.9.0.post0
@@ -100,14 +107,17 @@ sniffio==1.3.1
     # via anthropic
     # via anyio
     # via httpx
+    # via openai
 tokenizers==0.20.0
     # via anthropic
 tqdm==4.66.5
     # via datasets
     # via huggingface-hub
+    # via openai
 typing-extensions==4.12.2
     # via anthropic
     # via huggingface-hub
+    # via openai
     # via pydantic
     # via pydantic-core
 tzdata==2024.1