[Screenshot_2026-09-09-12-41-42-444] i’m sorry, this had to be shared. what do you get when working with Lean remotely, then you express a wish for custard tarts, the AI says three hail marys and you mention Tom Lehrer’s Vatican Rag? gitlab pull requests welcomed. Feature request (serious despite…

[image] locl: Lean Are you referring to Lean proof assistant? [image] Lean Programming Language Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code. I am asking because I am lo…

[image] d12rg / d12rg-hypergroup-lean · GitLab GitLab.com should give you the context, keywords, and so on. palomar registry is for scientific provenance, but given my knowledge of SAT Solvers for VHDL → VLSI work (nmigen - a registered Trademark, symbiyosis,…

For anyone following along who, like me, may not already know all of the terminology being used here, I put together a list of references. I read all three posts, since the third post adds quite a bit of context around Lean, hardware formal verification, and the remote/container workflow. Lean an…

thanks for this, Eric. nmigen is a registered Trademark Trademark Status & Document Retrieval and so is rust Trademark Status & Document Retrieval Roswell is the backend container system we all use - i could have the name wrong. Rosalind? apologies if i have the name wrong, i have birth cyanosis a…

[image] EricGT: So the progression from things such as custard tarts → Hail Marys → Tom Lehrer → Lean → formal verification → GitLab helps explain the title. :slightly_smiling_face: the best bit for me is that the lyrics are original, unprompted, on-point, and very funny

And now for something completely different

ChatGPT Use cases and examples

EricGT September 10, 2026, 7:53am 2

Are you referring to Lean proof assistant?

I am asking because I am looking at another topic and found this topic which might be of value with the other topic.

Topic		Replies	Views
Solving Gravity: The Ultimate Challenge for AI Research Use cases and examples research , science	12	1280	October 13, 2026
GPT-5.6-sol quality regression - Malformed commands and Unicode appear in model output Bugs bug , hallucinations , regression , 5.6	9	651	September 17, 2026
GPT Builder Or Programming Language? Community project	22	1185	October 13, 2024
What has ChatGPT Pulse done to help you? Community pulse	36	2237	July 1, 2026
Can GPT convert different sheet music codes? API	12	6018	April 21, 2023

And now for something completely different

Related topics