trostaft

?! When did that happen. Great!

There's (at least) 2 of us! Well, mine is a little minisforum unit, but the idea is all the same.

Well, if the thesis is that we're running the heavy work on a remote server that's less of an issue.

That algorithm won't converge anytime soon. A pre-conditioner (i.e. at least some apprentice wizardy) helps.

It was, but the comments on that post were insanely depressing to read. I'm a mathematician, and find myself largely hopeful and excited for its future, but being online this last week has been incredibly brutal due to the surrounding vitriol. It's an avalanche of negativity, and I'm largely not talking about that of my peers (though indeed, some of my peers). Most mathematicians I've spoken have been reasonable / positive, perhaps an effect of my field.

I really need to just stay off social media for like a month and keep talking IRL. Longer, if I know what's good for me.

MCMC = Markov Chain Monte Carlo

It's a way to approximately draw samples from a probability distribution. Crucially, it applies even when we only know the distribution up to a multiplicative constant which is a common ailment of many distributions in the computational uncertainty quantification field (not that we don't know the constant, but that it's usually computationally catastrophic to estimate it well).

Not much computational mathematics here, but I do see some of interest in the MCMC community. In particular, 139, 93, and 101 are very interesting. Also (I'm not too familiar), I remember attending some talks on the Crouzeix conjecture 325 attacks, should sharpen some rates for Krylov methods. Obviously need to read deeper, some of these don't have corresponding Lean formalizations.

Cool!

> Why aren't mathematicians excited about the frontiers being unlocked by AI?

Well, I wouldn't generalize based off of the thread OP (and people on social media, including me). I think a lot of us are very excited! Most of my collaborators are, including myself.

There's a lot of simultaneous social change that's accompanying these tools, not all of which is positive. Agonized screaming is pretty loud, relatively speaking to the rest of the conversation.

Indeed, I've switched over to model similar to this in the course I teach. Weekly optional problem set + in-class quiz every week with one homework problem verbatim + an extension. The homeworks are completely open resource, LLM, friend, sorcery, w/e. I figure that, even if they're given an oracle, they have to internalize the ideas to the point where they can generalize on the follow-up. I'll only really know when the course finishes, but I think this will work out. I want to pair this with an oral midterm and final, but that'll have to wait a semester.

You're talking about this article? I don't see how you could get that, fundamentally I read it the other way around. Unless you're talking about the base assumption of capabilities.

> As an ex-mathematician I assure you this is very wrong, and every working mathematician I know right now is completely miserable, and/or trying to flee the field as fast as possible.

To throw a counterpoint to this into the writhing cesspit of HN, I'm active in academic mathematics (postdoc) and every one of my collaborators is deeply in love with the field and their jobs. Perhaps the grass is greener on the applied mathematics side of the fence.

Am I doing my napkin math correct? The post says it's using a model comparable to Fable 5.1, which is $50 per million output tokens. So this is ~$300K? Surely an over-estimate due to caching.

Ah, interesting! I've been toying around with a formalizing of a paper I'm closing to submitting; maybe I'll try to clean it up into a format for this.

I'm teaching a university math course next semester and I've been messing around with a solution to this that my old analysis professor used to employ. Every week, they take home a handful of theory questions. These aren't turned in for credit. But, every week, there'll be a short quiz where one of those questions are asked verbatim, along with a small follow up.

That felt like a very natural solution to me. Of course, worst case scenario, they just blindly generate and memorize the proofs without thinking. But I think the follow ups will catch them in that case. Moreover, I choose to believe that >90% of my students are willing to at least put in the work of scrutinizing those proofs which is honestly not bad exercise in its own right.

I would love to do oral exams directly, the logistics with the number of students I have just make that hard. I know we're trialing it with the less populated special topics courses.

I've been curious of other publication quality figure generation libraries for python, if you have a moment I'd be interested as to why you chose Altair over plotnine? I'm well and truly entrenched in the Matplotlib style of plotting, so I appreciate any opinions here.

I've been using LaTeX for math for over a decade now. I'm pretty happy with it frankly, but there are major pain points in the compilation time and whenever it's time to interface with the language programmatically. Typst is, frankly, awesome in that regard.

However, I really dislike the 'magic' in the math mode syntax, and I think dropping backslashes (more generally, a delineator) for commands was a mistake. Those aren't blockers though, and I think the org is largely making good decisions. I'm really looking forward to the day I can write research in it!

I think all that's remaining is time in the community and stability. Once journals begin accepting it, I know I'll definitely try to submit in it.

Fantastic! It might be time for me to give it a shot again.

Truthfully, I like the more opinionated visual design of GNOME, but I moved to KDE long ago for VRR and better fractional scaling support. They just got it right and working. Huge props to the team, I know that's very difficult.

EDIT: On a side note, is anyone informed about the state of VRR + fractional scaling + general gaming on GNOME? Has it gotten better?

The upper tier features on the webapp are paid, but the local tools are all free. That includes local editor support. IIRC the compiler is apache 2.

> (multiple times, don't ask, yes, I've tried the one you're thinking of and it didn't work for me).

I know you didn't want questions, but maybe you can save me some trouble?

Assuming you're talking about quarto, may I ask what you didn't like about it? I've been converting some of my course materials to it and have been enjoying it immensely.

I'm desperately clutching onto my original steam deck. Some of the buttons are beginning to go, but it looks like we'll be holding onto it for another 1-2 years at this rate.

Waiting, in anticipation and horror, for the price of the frame.

This is still very much alive in the fighting game scene. At least in the US, every major city has at least one local running a bracket and casual sets regularly. This has many of them, not all: https://sk-tekken.com/tracker

I spent years grinding to learn mathematics because it was the language I needed to solve problems that excite me. If the tools I need to do so change, I can change too. Research training is not so rigid that it can only applied to the single set of skills I developed it in the context of. I can learn this too.

Moreover, truth be told, I don't really see myself doing any less math and requiring less from my skills. At least from the moment I've begun incorporating LLMs into my research workflow to now, the demand I've had from my own skills has only grown. At least in an era prior to Lean formalization.

That I'd agree with! I really need to get around to learning Lean myself. It might be interesting to try and formalize some missing theoretical pieces from my field (or likely start smaller).

Arguing similarly to how stockfish, the chess engine, trains I would not be surprised if this is more common in the future. I don't know if they use any proof verification tools during their reinforcement learning procedure right now, as far as I know they've been focusing more on COT based strategies (w/o Lean). But I'm hardly an LLM expert, I don't know.

Speaking as a postdoc in math, I must say that this is rather exciting. This is outside of my field, but the companion remarks document is quite digestible. It appears as though the proof here fairly inspired by results in literature, but the tweaks are non-trivial. Or, at least to me, they appear to be substantial to where I would consider the entire publication novel and exciting.

Many of my colleagues and I have been experimenting with LLMs in our research process. I've had pretty great success, though fairly rarely do they solve my entire research question outright like this. Usually, I end up with a back and forth process of refinements and questions on my end until eventually the idea comes apparent. Not unlike my traditional research refinement process, just better. Of course, I don't have access to the model they're using =) .

Nevertheless, one thing that struck me in this writeup, was the lack of attribution in the quoted final response from the model. In a field like math, where most research is posted publicly and is available, attribution of prior results is both social credit and how we find/build abstractions and concentrate attention. The human-edited paper naturally contains this. I dug through the chain-of-thought publication and did actually find (a few of) them. If people working on these LLMs are reading, it's very important to me that these are contained in the actual model output.

One more note: the comments on articles like these on HN and otherwise are usually pretty negative / downcast. There's great reason for that, what with how these companies market themselves and how proponents of the technology conduct themselves on social media. Moreover, I personally cannot feel anything other than disgust seeing these models displace talented creatives whose work they're trained on (often to the detriment of quality). But, for scientists, I find that these tools address the problem of the exploding complexity barrier in the frontier. Every day, it grows harder and harder to contain a mental map of recent relevant progress by simple virtue of the amount being produced. I cannot help but be very optimistic about the ambition mathematicians of this era will be able to scale to. There still remain lots of problems in current era tools and their usage though.

> A difficult part was constructing a chess board on which to play math (Lean). Now it's just pattern recognition and computation.

However, this was not verified in Lean. This was purely plain language in and out. I think, in many ways, this is a quite exciting demonstration of exactly the opposite of the point you're making. Verification comes in when you want to offload checking proofs to computers as well. As it stands, this proof was hand-verified by a group of mathematicians in the field.

I'm a computational mathematician, and I've been a big proponent of JAX to all the research groups I've worked with. So far, I've converted all of them =). In particular for math, I've found JAX's design and feature set to be far more suitable. Patrick Kidger's suite of libraries also carries a lot of weight in that regard. Equinox is the center is basically everything I write in JAX.

But there are absolutely pain points. In particular, especially for weaker programmers (common in academia), it's quite easy to write bad JAX. The functional programming and stateless paradigms require a little more thinking ahead. This is particularly tough when you're doing research and you're, in real time, finding out what's ahead!

Ah the JL lemma. Probably one of my favorite too. I'm teaching a mathematics of data course next semester, and even though we don't assume probability as a prerequisite I'm going to find a way to talk about that idea.

> eschatology

From Wikipedia

Eschatology (/ˌɛskəˈtɒlədʒi/; from Ancient Greek ἔσχατος (éskhatos) 'last' and -logy) concerns expectations of the end of present age, human history, or the world itself.

I'm case anyone else is vocabulary skill checked like me