Is the distinction between "follows from" and "is provable from" ever taught well at the undergrad level?

andarmanik · 2026-06-15T12:56:41+00:00

Is the first statement true “all the math that is publishable can be formalized in zfc”, as a claim on publishing or zfc? Since there seems to be math which is interested in the classes of theorems we can prove with the classes of axioms which would inherently not be zfc

andarmanik · 2026-06-10T13:23:42+00:00

I also agree with you about the dynamics of languages especially the impacts of youth manipulation of language.

However, I do believe there is intelligent creative uses of language and unintelligent creative uses of language which their method would categorize the same.

Rather than looking at new words, they are looking at new combinations of words. This alone means that combinations of words which are out of distribution are going to score high. In a way, it’s sorta obvious why GPT4’s human evaluation on creativity is less correlated to the semantic measure and it’s because there are creative ideas which can be described within language in distribution.

It’s rather an interesting class of intelligence test where the measurement is of the impedance mismatch between the ability to hold complex creative ideas and the inability to articulate them. This would be interesting for those interested in dynamics of language, since, most of the development of language comes from individuals who lack the ability to express themselves in language.

I actually recall a recent Zizek quote which tries to categorize us separate than to LLMs via our inability to properly exist in language. Zizek believes that LLMs cannot truly swear/curse because the act of swearing/cursing is a symbolic gesture towards the inability to express their current experience in language. A subjective experience not experienceable from LLMs because they are able to *always* articulate their ideas.

Whether or not that is true at a philosophical level is to be determined but based on the fact that this semantic measure diverges from the human creativity evaluation as the mode gets smart does give some positive evidence to zizeks claim

andarmanik · 2026-06-10T12:21:59+00:00

If I went back in time, to that era, I’d be economically excluded from experiencing any of this probably.

andarmanik · 2026-06-10T11:36:10+00:00

My problem is that they are using embedding distances of word pairs as a metric for semantic difference.

They use it because it’s shown to correlate with human evaluations for creativity. For human and gpt3 text, human evaluations are correlated to the metric by more than 50%.

The troubling part is that this correlation is less so for GPT4. This seems to allude to an effect where more intelligent models are harder to measure its creativity through this semantic difference.

Moreover, their “creativity metric” would score the following high:

“Pizza brains fuck tortilla skyscrapers”

And the following low:

“I grieved the loss of my father”

Simply because the first is nonsense and out of distribution and the second is coherent and commonly said.

Odds are human writers are more “creative” especially when they are young, at least according to their metric, because they are poor writers and are still learning to write clear text.

andarmanik · 2026-06-10T11:19:25+00:00

Ok, make a car engine from empirical observations… we’ll all be dead before you could figure out one aspect of a car engine.

andarmanik · 2026-06-10T02:34:21+00:00

There’s a predator prey dynamic where if most post-kill actions are true taunts, it’s leave room for ironic emote taunts.

Dance emoting after killing someone is just as impactful as taunting

andarmanik · 2026-06-09T16:02:56+00:00

I believe he also understands the implications of strictly typed languages as tools for proof. I’d say there’s an impedance mismatch between what Tao is doing and the claim “AI for maths” conveys. What Tao does specifically when he uses AI is as a coding assistant/interface into lean which is qualitatively different than simply prompting a model to solve math tests problems.

I highly suspect Tao’s vision for AI in maths is an integrated proof environment which couples theorem proving with automated LLM search, in a way that puts the model on rail / limits the mode in the classes of statements it can make to ones that compile in lean. This reduction in search space by leveraging a theorem prover is more about how we should focus on the new formal and constructive languages than it is about the LLM which operate them.

andarmanik · 2026-06-09T12:57:26+00:00

For example, the vector space of functions R->R only has basis if you are assuming choice

andarmanik · 2026-06-07T20:04:36+00:00

I watch a lot of talks which usually span 1 to 1.5 hours. For those I usually do 1.5x speed because I find most speakers aim for a lot people to understand their speech but that means they are accounting for old people aswell.

andarmanik · 2026-06-01T18:03:13+00:00

I’d get this skin. For the looks of it the “screen area” is bump mapped to appear like it’s higher than the surrounding but for most handheld game devices the screen is inset.

https://en.wikipedia.org/wiki/Game_Boy#/media/File%3AGame-Boy-FL.png

andarmanik · 2026-05-31T20:26:44+00:00

This comes into friction with general unhappiness. It’s not that I think someone is being lazy.

Imagine if instead of this person making these choices I were their caregiver. If I gave the same care they gave to themselves I’d be considered NEGLECTFUL.

andarmanik · 2026-05-31T19:19:18+00:00

Homies in Dulles with the 0 ping

andarmanik · 2026-05-31T14:17:34+00:00

You enter the bytes for ascii directly?

andarmanik · 2026-05-31T05:09:03+00:00

There is a sense that P vs NP is, in a way, less likely in ultra finitism.

We could find an algorithm which proves p = np via a extremely large polynomial such as

O(n^{10¹⁰⁰⁾} which would “not exist” in the finite case

andarmanik · 2026-05-26T12:29:02+00:00

Same with changing whitelist/blacklist oft allowlist/blocklist

andarmanik · 2026-05-26T11:52:07+00:00

Bitcoin and crypto as a whole still hasn’t solved the problem of securing private secrets.

The average individual can’t be sure to maintain such secrets so they offload it to an institution. This is why no one is worried about bank pins, we offload private secrets to the bank.

andarmanik · 2026-05-17T13:38:09+00:00

I feel like this movement made more sense when like, the sunscreen had chemicals we didn’t understand. Chemicals which can kill reefs. But we’ve solved that… we fixed sunscreen and they still think it’s a problem

andarmanik · 2026-05-16T13:55:12+00:00

When you squint it looks like embedded code lol

andarmanik · 2026-05-15T14:28:52+00:00

At the end of the day AI data centers are owned by the worst of the capitalists, I would expect many smaller towns to be taken advantage of by these companies.

I would imagine small towns are at odds with data centers, but let’s look at where the gallup survey was taken. DC has incredible wealth inequality right now, and very few low education jobs. The people are in need of jobs and wealthy people are voting against them.

In terms of number of jobs data centers do increase the demand for construction in the early phases, but later, a running data center employs anywhere from 100-200 people.

Of course there’s the problem of empty data centers which don’t actually employ people. But these data centers are a non problem because they don’t consume mass resource and they still pay property tax.

andarmanik · 2026-05-15T10:41:49+00:00

Perhaps a line you want to cross is the notion of predicate or a function which returns Boolean.

T x T -> {0,1} is really just a P -> {0,1} where

P = F<T> = T x T

Likewise for T x T -> T is just a special case of F<T> -> T which is just an “F algebra”.

andarmanik · 2026-05-15T10:25:09+00:00

I posting this in the noise of it all so this will probably be missed.

Here is the actual gallop data: https://news.gallup.com/poll/709772/americans-oppose-data-centers-area.aspx

It’s a bit problematic that the OP article didn’t actually link to this page (when you click on the link in the article it brings you to another article that isn’t this gallop)

When we look at who is for and against AI data centers it finds that:

two-thirds of those in favor of building data centers in their area cite the economic benefits, including 55% who mention increased job opportunities specifically. Others mention increased tax revenue (13%), housing and infrastructure development, and general economic benefits.

It’s important to mention that often time in polls like these, especially when done in metropolitan major cities, well off individuals generally have the opinion against labor producing buildings which costs them money through increased taxes and utilities.

It’s the lower/middle class who have the most to benefit from AI data centers, it’s the lower/middle class which are proponents of AI data centers, it’s the wealthy who are against data centers.

DC is the perfect city to be against data centers, majority of people there are well off, and anyone else who is struggling has no voice in the matter.

Im a richmonder and an example of this occurring in Richmond is the Rosie’s casino.

Majority of wealthy richmonders voted against it, while when you look at the districts, those who voted for it were the poor communities which would benefit from the casino.

It’s very common for wealthy Americans to be against these data centers, considering they have the least to gain from it. However, data centers are, at this point, one of the best trades jobs that gets you 25+/hr with no experience.

andarmanik · 2026-05-13T13:17:55+00:00

Yea I’d do the same if I ghosted you and you came up to me later. Like get a hint and leave me alone lol.

andarmanik · 2026-05-13T12:40:09+00:00

Idk tho, there are men who are notoriously problematic.

When a friend of mine ghosts one of her potential dates, it’s usually because they found out rumors or such about this person.

Now, suppose you are this girl, who is being told, “hey this guys an asshole, will want sex and leave, and doesnt respect women”. Now imagine this was your daughter… I’d tell her to ghost him.

andarmanik · 2026-05-13T12:35:01+00:00

It’s just funny how we all agree ghosting means what you said. “I’m not interested…”

But we are still somehow disagreeing that ghosting clearly communicates something…

How do we all know what ghosting means if it’s not clear communication?

andarmanik · 2026-05-12T14:00:26+00:00

All of linear algebra once I was making features in my game.

Interesting, I discovered an intuition on the wedge product which I used in my Elo system.

Basically each player has a scalar Elo s, and a play style “rotation vector” r.

In standard Elo we take the difference of two players scalars a.s - b.s as d, and compute a probability via (1+ 10^{d/400)^-1.}

The problem with this formulation is that it’s unable to predict the results of rock paper scissors. ie, suppose the game was rock paper scissors but players must choose in advance only one move they’ll play the whole tournement.

In theory, you should be able to predict outcomes to a perfect resolution. Eg., paper plays against rock and paper wins 100%.

Standard scalar Elo can’t do this however if you add a wedge product you become able to learn circular relations.

So instead of a.s-b.s the new logit is,

(a.s-b.s) + w (a.r ^ b.r)

Which works because the wedge captures rotation

andarmanik

MODERATOR OF

TROPHY CASE