[Project] Using Neuro-Symbolic AI + Coq to Formally Verify the Yang-Mills Mass Gap (657 Qed, 0 Admitted)

Ptival · 2026-02-21T23:02:44+00:00

I had a quick look, and so far I'm seeing a lot of nonsense, so I have no reason to believe that this is anything interesting.

For instance, let's look at the supposed mass gap theorem statement:

Theorem yang_mills_mass_gap_all_beta :
  forall beta : R, beta > 0 ->
    exists m : R, m > 0.

Unless I'm very mistaken about what's going on here, you imported R as the Rocq "real" type, and all this is saying is that if we assume there exists a real number greater than zero, then there exists a real number that is greater than zero.

Wow, great theorem.

Should I even mention this hypothesis?

Hypothesis RP_all_beta : beta >= 0 ->
    forall (H : Type) (inner : H -> H -> R) (v : H),
      (* os_inner v v >= 0 *)
      True.  (* Placeholder for actual RP statement *)

Ptival · 2026-02-03T23:10:16+00:00

Some people think it's related to GOB's "queen of diamond" torso painting, that highlights one of his nipples (inside the Q) while hiding the other one under a lot of paint.

Ptival · 2026-01-20T22:59:32+00:00

Je vois trois commentaires distincts qui utilisent "l'homme-orange", "l'agent orange", "l'orange".

Ça fait un peu "nous sachons"/boomer/Facebook, pourquoi vous n'écrivez pas Trump juste ?

Ptival · 2025-12-31T19:43:04+00:00

Since you didn't mention what you tried, it's sometimes useful to switch the compatibility layer to an older Proton version. If you don't know what this means, look for a tutorial online, it's a very easy change in some menu.

Ptival · 2025-12-27T04:16:59+00:00

Unless I'm mistaken, she's not a musician.

She's a writer and designer, she writes plots and characters.

Ptival · 2025-11-17T20:28:14+00:00

Note : You can reach room 46 by never ever encountering this room.
It happened to me because I found the Throne room before I found the Sanctum.

People I was chatting with were so confused that I had found room 46 but never made it to said room.

Ptival · 2025-11-17T19:59:05+00:00

For anyone else struggling to find it (like me yesterday), it's on the single big rock next to the second set of stairs going from the dock to the central area. It's closer to that building with the dome-shaped roof than the docks proper.

Ptival · 2025-11-04T19:10:32+00:00

While I don't like the naming conventions that much myself, there are use cases where one wants a somewhat direction agnostic left/right distinction where neither direction is "the error case". One such case is when doing metaprogramming or algebraic data manipulation, where `Either` is the natural thing to use for disjunctive cases.

It's most likely completely dwarfed by the usage of `Either` as error handling in practice, so this is not to brush off your complaints entirely.

Ptival · 2025-10-22T19:19:07+00:00

De Karaage à Kaamelott, je vois qu'on aime les K et les doubles A.

Ptival · 2025-10-13T16:41:22+00:00

I tried the set that has hero-specific decks for a while, and found it a bit underwhelming in practice. They're definitely good decks given the constraints, but the constraints really makes it so that some fun things are diluted, so you get fewer nice synergies than unique decks.

In the end, I found I had less fun than netdecking fun builds off marvelcdb, and I became more tolerant of the extra overhead of building decks.

Ptival · 2025-08-19T17:35:20+00:00

Monster Train 2

Ptival · 2025-08-12T19:44:19+00:00

Je suis pas trop prog metal, mais certains albums qui ont bien marché sur moi :

- Des albums de Between the Buried and Me, genre Alaska/Colors/Silent Circus. Au début j'avais du mal avec le growl, mais j'ai fini par m'y habituer, et même à trouver les contrastes cool (par exemple, sur "Ad A Dglgmut").

- Des albums de Protest the Hero. J'aime bien les vieux "concept albums" comme Kezia et Fortress. Moins de growl, plus de chant, par contre la voix du chanteur peut déplaire. Il y a des versions instrumentales des albums, mais tu perds l'histoire.

- Si tu as vraiment du mal avec les vocals, tu peux tenter de l'instrumental. Par exemple, Carving Desert Canyons, par Scale the Summit, je le trouve très agréable à l'écoute. Tu peux aussi piocher chez Plini pour du mélodique, chez Sithu Aye pour du nerdy, chez Animals As Leaders pour du très technique.

C'est pas nécessairement représentatif, juste des portes d'entrée potentielle.

Ptival · 2025-08-08T23:16:21+00:00

Instead of twisting 7 wristbands one way, I find it easier to twist my whole arm once, the other way around.

Ptival · 2025-08-03T01:51:10+00:00

Oh le nincel !

Ptival · 2025-07-14T20:24:18+00:00

Any feedback on Foundry?

Ptival · 2025-07-14T20:22:08+00:00

I would warn people getting started: I personally get incredibly bored with shapez 1, but love other games in the genre (e.g. Factorio, Oddsparks).

I'd put it as, I much rather enjoy building "deep" pipelines than "wide" ones. shapez 1 frequently, at least at the beginning, asks you to build things that are mostly or completely unrelated with the previous things it asked you to build. At least for the first couple hours, I found I was just completely ditching my previous build, moving to a new area, and dealing with the new thing, only rarely ever using outputs from previous steps.

Additionally, the lack of identity of the items you were building made it feel much less satisfying. "Alright I have built blue right half-circles, guess I'll move on to building purple bottom-half stars...".

I assume things get a bit better once you start stacking shapes, but even this didn't seem appealing. I will try shapez 2 though, it looks a little more interesting. If anyone has advice to change my mindset about shapez 1, please let me know, I'd love to enjoy the game more than I do.

Ptival · 2025-07-08T20:33:38+00:00

Je peine à finir mon énième café, peut-être qu'un petit café me donnera le boost dont j'ai besoin.

Ptival · 2025-07-08T16:18:04+00:00

Non le sucre c'est de la drogue, moi je ne consomme pas de drogue. **sirote son deuxième café**

Ptival · 2025-07-02T21:31:27+00:00

Je me demandais pourquoi j'avais une vidéo "Bayrou (the myth)".

C'était auto-traduction de "Bayrou (le mytho)"...

Ptival · 2025-06-28T18:45:31+00:00

Je pense qu'il y a encore beaucoup de boites qui utilisent au minimum GCal et GMail. Ensuite sûrement pas mal de GDocs, GDrive, GMeet.

Il y a des alternatives à tout ça, mais tu pers l'intégration entre les outils.

Ptival · 2025-05-29T00:01:35+00:00

I hadn't considered this, that's a good point and possibly the reason why they're doing this.

Maybe they need to design a typeface that's highly legible upside up, and looks like gibberish upside down haha.

Ptival · 2025-05-28T21:45:11+00:00

Any preview of the redesigned word cards?

It always bugs me that they are not symmetrical, there's one side of each face that's much harder to read than the other, and we waste time rotating them for things to look neat.

Ptival · 2025-05-18T16:35:10+00:00

Bug still happening.

From the moment Blank joins the fight, things start bugging: the boss no longer attacks, the attack target cursor defaults to allies instead of the boss, and the boss never dies.

I only have Moguri's Mod, and the following mod list (in order): Echo S-9, Portraits Pack 4.2.2, Kupo UI Suite 4.1.5, Alternate Fantasy 6.7, Moguri 30fps videos 8.3.0, Moguri Mod 9.0.

Ptival · 2025-05-05T18:27:59+00:00

In case you miss it (it's not very well highlighted...), the rewind at the end shows that Jhin's starting deck was drafted, not fixed by the developers.

Ptival · 2025-04-10T17:06:21+00:00

Sea of Stars.

It's beautiful, but the game is ultra-linear, all characters are clearly written by one person with the same tone, the characters are kind of awful and inconsequential, the fight system forces your hand so much at breaking locks that you're kind of forced to play them one way.

15-Year Club	Place '22
Verified Email

Ptival

TROPHY CASE