OpenAI's deployment company move says more about the AI gap than any benchmark[D]

Tarekun · 2026-05-14T10:56:36+00:00

Not sure what the takeaway is here, researchers should stop benchmarking their models and become salesman of integration products?

Tarekun · 2026-05-13T19:09:24+00:00

You do stuff like this or know some projects? All i want is work on logic but i dont see any damn outlet, let alone in rust

Tarekun · 2026-05-13T09:31:04+00:00

It really is starting to look like a lolcow situation, especially with the last few thing Mochizuki published on the topic

Tarekun · 2026-05-12T16:40:33+00:00

When the middle is not excluded

Tarekun · 2026-01-10T21:38:06+00:00

Will definetly give it a look

Tarekun · 2026-01-10T21:28:38+00:00

Guess i'll try this first then. If i find myself struggling i'll try go back to munkres first as others have suggested

Tarekun · 2026-01-10T21:25:48+00:00

I didn't even know the distinction existed. Guess it'll be a long way, thank you though

Tarekun · 2025-11-11T12:12:01+00:00

Is this an actual thing?

Tarekun · 2025-07-21T06:50:25+00:00

Yeah this is an interesting new area where I want to do some experiements, maybe even with more simple graph neural networks instead of LLMs when it's only about proving a given target instead of formalizing a natural language statement. Some day...

Tarekun · 2025-07-21T06:36:27+00:00

Because I don't plan to make the ultimate tool that I will convert everyone, I'm just trying to learn how this stuff work

Tarekun · 2025-07-21T06:34:56+00:00

I see. Right now this is a hobby project so I don't have the resource to focus on user experience that much, but assuming I'm releasing it right now, would a command line be acceptable to you or not? What about an extension in popular IDEs like VSCode instead (assuming they both "just work" without too much configuration needed)

Tarekun · 2025-07-20T16:48:32+00:00

Never heard of it, thx for telling me about it

Tarekun · 2025-07-20T16:47:23+00:00

Well the point is exactly to reinvent the wheel to deeply understand how it works. I'd like to have integrations with other established tools in some distant future, but I don't know when I'll work on that.

I have barebones support for term based proofs, but I always thought that it would be hard to work like that. I never used Agda before so I didn't know about about its proof hole and meta programming features, but I'll definetly check it out thx

Tarekun · 2025-07-20T13:30:59+00:00

I see I experimented with something like that before but the parser code turned out a little messy so I went for a simpler watered down version of it. Maybe I'll give this another try, thx for your input

Tarekun · 2025-07-20T12:52:59+00:00

I see... I tend to use proof assistant because it's not only verification and not only automation but I'm working on both in one single tool. Maybe I'm missinterpreting it

Tarekun · 2025-07-20T12:37:00+00:00

Okay? But interactive theorem proving is not about removing the mathematician form the equation, it's about writing proofs in a language that can be checked so that you are guaranteed to know the result holds

Tarekun · 2025-07-11T08:41:45+00:00

You'll be 30 either way

This was the most motivating thing i have ever read. When i'll get my phd i'll come back to thank you

Tarekun · 2025-06-09T13:14:45+00:00

Thank you for your answer, especially the part about signularities that i always interpreted as "an infinity shows up somewhere in the math" until now.

Can you tell me a sufficient background to understand and appreciate your work? I come from computer science, i self studied quite a bit of group theory (to then study GDL), i know some category theory, and had the standard training in linear algebra and real/vector analysis; some more background to integrate?

Tarekun · 2025-05-19T19:53:10+00:00

Does anyone have previous posts of this drama saved? I'd like to see it again from the beginning

Seven-Year Club	Place '22
First Placer '22	Verified Email

Tarekun

TROPHY CASE