flaviat

joined 2 years ago
 

Announcement of the Agda fork by amy@types.pl:

The Agda developers have recently proposed codifying their official stance on LLM-generated contributions: they are "concerned about the negative effects of large language models (LLMs) on many individuals, our society, and our planet", but refuse to take any concrete action to address their own contribution to these.

Other extensions to the type theory are kept despite known inconsistencies (sized types), or being impossible to adopt without complete vertical buy-in (cumulativity, erased cubical), or simply for backwards compatibility (--guarded/@lock). In the best cases, these features are championed by a single maintainer, and keeping them well-tested against the continuous adoption of new features is a struggle when very little code uses them. Our plan is to focus on exactly one variant of the language ("full --cubical"), and to drop support for all the language features which are explicitly deprecated, inconsistent, or simply ill-understood in conjunction with this fragment.

I tried it out using Amélia's library (https://1lab.dev/) to show that free modules are projective. This is known to be equivalent to the axiom of choice and that informed the definition of projective to have mere existence of the lifted homomorphism. It was pretty ergonomic, details regarding homotopy levels were handled by hlevel and universe levels weren't bad. Automatic proof search worked with a sufficiently fleshed out structure

[–] flaviat@awful.systems 5 points 1 month ago (9 children)

I just entered university for math and even though this is all very demotivating, it's just what I'm good at.

https://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/

The AI people's cry of "no don't look at the code! it's in lean so it's correct! does give me a bit of hope (hi bitofhope if you're here) that it's bullshit that will fall over

[–] flaviat@awful.systems 5 points 1 month ago

Smart Pipe Inc. is a Registered Sex Offender

[–] flaviat@awful.systems 5 points 2 months ago (3 children)

There cannot be such a thing since pdf does not structure its data. There is an extension to the standard that would let a program do it for you but nobody uses it (PDF/UA-1). (also pandoc is vibe coded now)

[–] flaviat@awful.systems 5 points 3 months ago

+1 for Archipelago

[–] flaviat@awful.systems 4 points 3 months ago

OMG I just installed it! Great to see.

[–] flaviat@awful.systems 4 points 3 months ago

I believe it's the "don't stuff beans up your nose" effect, writing this prompt is causing it to mention goblins

[–] flaviat@awful.systems 3 points 4 months ago

Bravo. The farthest i could get is 2/3 assuming the following model: x₁ is a random number between 0 and 1, x₂ between x₁ and 1, and so on. If the service breaks at x₁, gets fixed at x₂, breaks again at x₃, etc. availability is 2/3.

[–] flaviat@awful.systems 8 points 6 months ago (1 children)

Luna is a very common transfem name

[–] flaviat@awful.systems 5 points 7 months ago

I also had a computer not boot. Tried installing windows 11 but the iso does not include network card drivers and requires a second drive that has them. I just happened to have another but it malfunctioned. Was assured IT would fix it but it still doesn't boot. :(

[–] flaviat@awful.systems 14 points 7 months ago (2 children)

This github bot arguing with itself for over 5000 comments over an issue label

https://github.com/google-gemini/gemini-cli/issues/16723

[–] flaviat@awful.systems 4 points 7 months ago* (last edited 7 months ago)

Thank you for the links

Junk theorems in Lean are laughably bad due to type coercions.

Those look suspicious... I mean when you consider that the set of propositions is given a topology and an order, "The set {z : ℝ | z ≠ 0} is a continuous, non-monotone surjection." doesn't seem so ridiculous after all. Similarly the determinant of logical operations gains meaning on a boolean algebra. Zeta(1) is also by design. It does start getting juicy around "2 - 3 = +∞" and the nontransitive equality and the integer interval.

view more: next ›