It's pretty wild that the author gets a somewhat-usable result merely by few-sho... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		blueblimp on Aug 16, 2022 \| parent \| context \| favorite \| on: The future of interactive theorem proving? It's pretty wild that the author gets a somewhat-usable result merely by few-shot prompting OpenAI Codex.

riku_iki on Aug 17, 2022 [–]

probably codex was trained on lean code too.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact