Cheng Zhang

Assistant professor at WPI; coalgebra, Kleene algebra, and programming language practitioner.

"I cannot Grothendick construction under these conditions."

Pronouns: he/him or they/them

Public Key

npub1ucfl35l5pyknn8j3yhghqjljmllxsmmtjggkuxfpu782nnrfj0wqd8q6qy

NIP-05 Address

czhang03_at_mathstodon.xyz@momostr.pink

Profile Code

nprofile1qqswvylc606qjtfenegjt5tsf0edllngda4eyytwrys70r4fe35e8hqpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0ds96nlfd

Publishing to

relay.damus.io

nos.lol

Author Public Key

npub1ucfl35l5pyknn8j3yhghqjljmllxsmmtjggkuxfpu782nnrfj0wqd8q6qy

Show more details

Last Notes

2026-04-22 23:08:46 UTC

- reply

I suspect I know who you are talking about, and I am happy to report, they are still saying that now :) (but only in the context of trashing other proof system)

2026-04-20 00:12:53 UTC

- reply

Science is happening!

2026-04-16 15:04:28 UTC

The typical "smart person" depiction in popular media behaves exactly like a computer: they can calculate really fast, and/or remember a lot of things quickly and accurately.
I suspect this depiction might stem from the lack of understanding for human ingenuity by the public, which can also explain why many conceive LLM, a device aimed to remember and imitate human text, is "intelligent".

2026-04-16 11:32:32 UTC

- reply

slopal method v.s. formal method.

2026-04-11 13:15:28 UTC

- reply

I think Mythos is probably good, and much better than what I expected LLM can do in recent years.
But to me this is an cool alternative, and compensate the current security research.
Where security research can archive much better result per dollar, security research never gets the same amount of attention and investment as these LLMs.

2026-04-11 12:59:41 UTC

- reply

Okay I am most talk about inference cost, and trying to be conservative in estimate. Yes, but training cost should be around 10k if not 100k more expensive than traditional research.

2026-04-11 12:54:00 UTC

I am trying to be very cautious in being under representing current AI's ability, but I find the whole marketing behind mythos a bit over blown.
It is not uncommon for a year-long research project in verification and fuzzing to find tens of bug in critical software. Then we learn from them, integrate it into standard fuzzer and checker, so bugs of these nature reduces dramatically.
I guess I am not understanding (or arguably, a bit salty) that suddenly there is something that consume 100 times more resource than what we have developed found more bugs, they are "too dangerous", as if security research and software in general are doomed.

2026-04-02 22:46:08 UTC

New Career Goal: developing a framework surrounding Elgot iteration (often written as dagger) called Caesar.

2026-04-01 19:41:32 UTC

- reply

And violation of AGPL for not including your logo.

2026-04-01 11:47:09 UTC

Happy to report, my latest research is done completely autonomously with ✨AI✨: I snapped a picture of a commutative diagram in my note, and it fully autonomously generate the tikzcd diagram. I haven't written any tickzcd code by hand in the past year.
Ladys and gentleman, category theory is solved, by ✨AI✨

2026-02-10 00:27:34 UTC

- reply

There is an ocaml gradescope library https://github.com/qcfu-bu/gradescope_ocaml/ assuming this is what you are looking for.

2026-01-28 01:01:10 UTC

- reply

But what does the fox say?

2026-01-02 22:41:06 UTC

Spend $500 on RAM so that I can open three electron app on a zoom call.

2026-01-02 12:35:04 UTC

- reply

Hey Prof. Jacob, it seems like I cannot access the paper from this URL, can you double check if the URL is correct?

2025-09-20 20:20:11 UTC

unlike donut-shaped donut or mug-shaped mug, donut-shaped mug is neither homoemorphic to donut nor mug.
https://media.mathstodon.xyz/media_attachments/files/115/238/476/906/686/792/original/b917f74a12aec777.jpg

2025-08-28 23:02:15 UTC

Who call them "categories" when "monoid-oids" is right there?!

2025-08-26 14:13:01 UTC

- reply

I feel there are two notions of "languages" here: the first is tooling and the second is foundation.
While the tooling to understand semantics have rapidly modernized in the recent several decades, the foundation is still the same.
This means that you can recover the classical domain literature by specializing modern ones, establishing these connections.
However, a lot of the theorem within Haskell often arises from an idealized fragment, since the full semantics of any industrial programming language is just intractable to reason about within one's mind. Yet, such idealized fragment is never formalized in mathematics. I think this is akin to the idea in https://math.andrej.com/2016/08/06/hask-is-not-a-category/
So, I feel trying to establish connections with coding-focused paper necessarily need to sacrifice formality in order to recover the idealized fragment the original author have in their mind, since again, the full semantics of Haskell is too gigantic, and clearly out of scope for most papers.

2025-08-22 12:56:45 UTC

We should make a new version of Lean using Bool instead of Prop, and call it Boolean.

2025-08-20 10:50:21 UTC

I think there needs to be a category of PL works named "SMT and prayers".

2025-08-15 08:37:24 UTC

If all road leads to Rome, all road also leads to anywhere else with a road.

2025-08-11 19:34:32 UTC

- reply

Indeed the weakest part of my papers are always my research.

2025-07-26 07:31:44 UTC

My research stands between theory and practice.
That means I get to suck at both programming and math.

2025-07-25 18:33:07 UTC

Got some Prolog today with @npub1v6a…c7s4
https://media.mathstodon.xyz/media_attachments/files/114/915/303/746/939/356/original/67e2a2b705781acd.jpg
https://media.mathstodon.xyz/media_attachments/files/114/915/304/235/479/053/original/6f6430b46489571f.jpg

2025-07-02 13:40:48 UTC

Nowadays, the primary drive for my researches is to publish papers with puns in their titles.

2025-06-15 16:00:04 UTC

(• − •)
https://media.mathstodon.xyz/media_attachments/files/114/688/205/268/636/865/original/abee30ae3ae3bb9f.png

2025-06-14 11:35:55 UTC

Math is the only kind of magic where peeking behind the curtain only makes it more fun.

2025-06-09 15:00:27 UTC

Showering is probably the most important invention for scientific advancement.

2025-06-07 19:33:57 UTC

"I am not perfect... I am perfectoid."

2025-05-27 08:54:05 UTC

Data flow is the worst thing that has ever happened to control flow.

2025-02-22 18:22:43 UTC

Bun made it very clear that they are "NOT AVALIABLE"
https://media.mathstodon.xyz/media_attachments/files/114/048/929/814/481/890/original/355eaa4a7bdcc261.jpg

2025-02-17 21:31:49 UTC

Should we build more parks or parking?
https://media.mathstodon.xyz/media_attachments/files/114/021/361/804/207/183/original/25ad3991264d383f.jpeg

2024-11-20 08:16:34 UTC

Contrary to popular American belief, fallen leaves don't bite if you don't point a noisy, smelly, polluting air gun at them.
It is also okay to let grass grow taller than 5cm.
https://media.mathstodon.xyz/media_attachments/files/113/514/288/856/438/823/original/7bb9bf595adf2888.jpg
https://media.mathstodon.xyz/media_attachments/files/113/514/289/070/618/575/original/3d56ace89a856e10.jpg

2024-10-31 22:15:07 UTC

Breaking News! Great Britain just invented Tater tots!
https://media.mathstodon.xyz/media_attachments/files/113/404/327/943/098/334/original/eba503ee38c79f2d.jpg

2024-10-13 15:32:57 UTC

- reply

There is a reason to my madness. As I am planning on leaving the U.S. for my postdoc. I am making some sauces that will help my wife cook.
I was planning garlic sauce (for stir fry), spicy chicken stew base (烧鸡公底料, despite its name, can do almost all spicy stew, and even some stir fry), and chard chili sauce (go into cold dish and can be eaten straight with rice or noodles).
Now, in the light of my 5lb garlic purchase, I have garlic sauce, garlicky spicy stew, and garlic chard chili sauce. Fortunately, my wife really really likes garlic 🤪.
https://media.mathstodon.xyz/media_attachments/files/113/300/835/582/206/341/original/fbaeb850ff68eed7.jpg

2024-10-12 21:49:54 UTC

After having a laugh at @npub1f20…d5dd 's 5lb of New Mexico pepper with my wife, I, in my infinite wisdom, brought 5lb of raw peeled garlic.
https://media.mathstodon.xyz/media_attachments/files/113/296/657/193/132/797/original/4520d0d711981dc8.jpg

2024-10-04 00:41:21 UTC

- reply

Pfff, almost forgot the most important one...
https://media.mathstodon.xyz/media_attachments/files/113/246/370/570/981/643/original/823cdaea57241039.jpg

2024-10-04 00:26:21 UTC

rate my setup
https://media.mathstodon.xyz/media_attachments/files/113/246/311/512/266/309/original/10e57e36dff08ddc.jpg

2024-09-29 14:04:34 UTC

DO **MORE** NIGHTMARKET!
https://media.mathstodon.xyz/media_attachments/files/113/221/216/786/570/366/original/1fd06a24605fb26a.jpg
https://media.mathstodon.xyz/media_attachments/files/113/221/216/942/037/274/original/41b4fb4c8c4567ee.jpg
https://media.mathstodon.xyz/media_attachments/files/113/221/217/118/189/819/original/abf1020d43a2def5.jpg
https://media.mathstodon.xyz/media_attachments/files/113/221/217/275/304/974/original/f68da4207c12cf23.jpg

2024-09-18 15:49:20 UTC

I currently have a plain text single page website (https://czhang03.github.io/). I used to enjoy the plain-text aesthetic, but recently I started to feel that the page is getting too cluttered and do not draw people in anymore.
Should I keep plain text, or do whatever hip CSS thing that people use?

2024-08-15 00:35:55 UTC

Not too bad for a initial sticker bomb
https://media.mathstodon.xyz/media_attachments/files/112/963/233/651/720/286/original/4016ce578a9f8f6a.jpg

2024-08-02 20:31:21 UTC

Do I sticker bomb my laptop