As a mathematician, I am looking forward to the day when nearly all of undergraduate mathematics and many of the lower level grad school math books are encoded in Lean (a proof checking language). Often I find that theorems are not stated precisely enough and I have trouble finding the exact statement of a theorem without digging through math books in my library. It would be nice if we put the physics and chemistry books into Lean also.

Simplifying all of math is another endeavor, but I imagine that you could have a bunch of LLMs trying to shorten existing Lean proofs.

I was pretty upset when my algebra professor tried to make us learn proof about n-dimensions matrices and what not. It was an undergraduate engineering degree and the vast majority of the formulas would mostly have up to 3 or 4 dimensions. That derailed the whole year (it's not like maths was the only subject). Complete proofs and theorems have their places, but learning stuff do need levels. The spherical model of the earth is good enough in 2nd grade (when we were first learning about geography (continents, seas, mountains, plains,...)), no need to do a full treatise there.

Reading that, the execution is now deterministic but the soundness is still probabilistic and <100%, no? Unless I'm reading it wrong.

Here is another list of ideas in math made by a lesser math person. (top 100 most useful)

counting zero integer decimal positional notation 100, 1000, … the four arithmetic operations + – * / fractions decimal notation 0.1, 0.01, … basic propositional logic (Modus ponens, contrapositive, If-then, and, or, nand, …) negative numbers equivalence classes equality & substitution basic algebra – idea of variables, equations, … the idea of probability commutative and associative properties distributive property powers (squared, cubed,…), – compound interest (miracle of) scientific notation 1.3e6 = 1,300,000 polynomials first order predicate logic infinity irrational numbers De Morgan’s laws statistical independence the notion of a function square root (cube root, …) inequalities (list of inequalities) power laws (i.e. abac=ab+c ) Cartesian coordinate plane basic set theory random variable probability distribution histogram the mean, expected value & strong law of large numbers the graph of a function standard deviation Pythagorean theorem vectors and vector spaces limits real numbers as limits of fractions, the least upper bound continuity Rn, Euclidean Space, and Hilbert spaces (inner or dot product) derivative correlation central limit theorem, Gaussian Distribution, Properties of Guassains. integrals chain rule modular arithmetic sine cosine tangent π, circumference, area, and volume formulas for circles, rectangles, parallelograms, triangles, spheres, cones,… linear regression Taylor’s theorem the number e and the exponential function Rolle’s theorem, Karush–Kuhn–Tucker conditions, derivative is zero at the maximum the notion of linearity Big O notation injective (one-to-one) / surjective (onto) functions imaginary numbers symmetry Euler’s Formula eiπ+1=0 Fourier transform, convolution in time domain is the product in the frequency domain (& vice versa), the FFT fundamental theorem of calculus logarithms matrices conic sections Boolean algebra Cauchy–Schwarz inequality binomial theorem – Pascal’s triangle the determinant ordinary differential equation (ODE) mode (maximum likelihood estimator) cosine law prime numbers linear independence Jacobian fundamental theorem of arithmetic duality – (polyhedron faces & points, geometry lines and points, Dual Linear Program, dual space, …) intermediate value theorem eigenvalues median entropy KL distance binomial distribution Bayes’ theorem 210≈1000 compactness, Heine – Borel theorem metric space, Triangle Inequality Projections, Best Approximation 1/(1−X)=1+X+X2+… partial differential equations quadratic formula Reisz representation theorem Fubini’s theorem the ideas of groups, semigroups, monoids, rings, … Singular Value Decomposition numeric integration – trapezoidal rule, Simpson’s rule, … mutual information Plancherel’s theorem matrix condition number integration by parts Euler’s method for numerical integration of ODEs (and improved Euler & Runge–Kutta) pigeon hole principle

mathematical used less often: Baire category theorem, Banach Spaces, Brouwer Fixed Point Theorem, Carathéodory’s Theorem, Category Theory, Cauchy integral formula, calculus of variations, closed graph theorem, Chinese remainder theorem, Clifford algebra (quaternions), Context Free Grammars, countable vs uncountable infinity, Cramer’s Rule, cohomology, Euclidean algorithm, fundamental group, Gauss’ Law, Grassmannian algebra , Graph Theory, Hahn-Banach Theorem, homology, Hairy Ball Theorem, Hölder’s inequality, inclusion-exclusion, Jordan Decomposition, Kalman Filters, Markov Chains (Hidden Markov Models), modules, non-associative algebras, Picard’s Great Theorem, Platonic/Euclidean solids, Principle of Induction, Probabilistic Graphical Models (Bayesian Networks, Markov Random Fields), Pontryagin duality, Quaternions, Spectral Theorem, Sylow p subgroup, repeating decimals equal a fraction, ring ideals, sine law, tensors, tessellation, transcendental numbers, Uniform Boundedness Theorem, Weierstrass approximation theorem. From http://artent.net/2012/11/27/100-most-useful-theorems-and-id...

Your lists formatting got eaten by HN.

For years I've had an idea in my head to add a Forth to the old game Master of Orion so that I could automate some of my common actions in the game. There is an open source GIThub called 1oom with source code for the game and I thought I would just write my own Forth. Well, I've recently been using AI's to code, so I asked GPT and it suggested that I use ficl rather than writing my own Forth. It helped me add ficl to 1oom. I've added Forth words to access most of the game variables and I've just begun adding forth words that can manipulate the game state. It's been fun. I had not written much, if any, Forth code in the last 30 years, so it's been a fun trip down memory lane.

I remember seeing the Amiga bouncing ball demo and being amazed.

https://www.youtube.com/watch?v=-ga41edXw3A

The Amiga was the second computer that I ever owned. The first was a C64 that I bought freshman year. (My father bought a TRS-80 before that.)

Certainly most universities now have a very strong liberal bias. I think most science departments were left leaning in the 1950s, but it is stronger now. (I think colleges and universities have always been more progressive than the general populous.) The administrations of universities are now very strongly Democrat leaning. I think that Trump just sees a lot of Democrat run institutions and thinks, "Why should the government support these institutions run almost entirely by Democrats."

Because until this administration, it has been considered a vital principle of democracy that the elected government supports all the citizens and institutions of the nation, not just the ones that it controls.

But principles don't exist out of nowhere. We had a very partisan country in the past. Consensus was built to get us here, then we just stopped putting in work on building/keeping consensus and resorted to Jon Stewart style calling/making people look like idiots, and expecting past consensus to hold things together in a Jon Stewart style world of mockery of each other. Consensus requires respect each way. One side threw it out the door (knowing or not) with Jon Stewart style ridicule of other but is shocked when that then got responded to X100 with Trump style politics.

> What did they expect would happen? Trump to just continue funding these people that hate him?

So you believe it's expected that a president will de-fund everything that supports their opposing party? I'm sure that's a totally great idea that won't cause any issues whatsoever.

American politics are so absurd.

Honestly, yes. I would expect that, or at least whichever party controls Congress to defund efforts that would seek to hurt them. The real abberation is that university funding has gone unscathed for so long. It's said too much and honestly I hate it, but consider the hypothetical: what if 80% of professors expounded right wing ideologies for about, 60 years? Would you not expect some kind of backlash?

I’m sure the same justification was trotted out in Hungary when they purged the intellectuals there, too.

Eh, I think there's a bit of a logical jump between "professors hate Trump" and "professors are expounding left-wing ideologies".

Yes, most professors are opposed to Trump. But when you're talking to a professor of, say, metallurgy, he's not using his classroom to rant against Trump. He's using his classroom to teach students about metallurgy, which is a pretty dang useful service to a modern industrial economy. Professor's personal political views aren't interfering with the economic and scientific value he's providing to the country.

Which is why the universities and research centers have largely been untouched until now. Until Trump, both sides could recognize that even if there was political disagreement between the professors and the politicians, the professors were still doing important work.

Trump took it personally, and on that personal basis he's now eroding our scientific and technological future. We're eating our seed corn, here.

> What did they expect would happen? Trump to just continue funding these people that hate him?

Never before in my recollection has U.S. national science policy been tied so closely tied to personal fealty to the president. It is alarming that you see nothing wrong with the connecting science funding to political alignment. This is highly aberrant.

In any case, if a majority of academics despise Trump and lean leftward overall, then maybe it would be a moment for self-identifying Republicans to gaze into the mirror and see what might be the reasons for this. As an academic, I have a commitment to the truth. This administration has no such commitment. This has been thoroughly documented.

This is has been significantly overstated my entire life - people making this claim always point to the women’s studies faculty and don’t mention how many engineering, Econ, law, etc. faculty are more conservative — but it more deeply misses the cause, as well. As the Republican Party purged internal dissent, that pushed people out who might have otherwise been on board for things like their fiscal or foreign policy positions but weren’t willing to say gay people were less than fully human or rejected the war on science. That last one is huge for universities because for most of the current century being a Republican has required rejecting the scientific consensus on climate change, the most pressing issue of our time, as well as other topics like public health or the separation of church and state. Criticizing universities for not having more people who reject their foundational principles is badly missing the point.

I used to know a Republican lobbyist who worked on environmental issues. He used to represent the coalition of fishers, hunters, hikers, bird-watchers, etc. who valued healthy forests, water, etc. but that line of work disappeared when they put out the fatwa against giving Obama any legislative wins even on issues which have broad public support and it never really came back because the party leadership decide that they represented industry first and only. Those people didn’t suddenly become liberals, the party moved away from them.

I'm retired. I hope to get a 3% per year income from my savings every year after inflation and taxes. If my state implemented a 1% wealth tax on savings each year, I would go bankrupt in 20 years. I am hoping that I will live 20 years.

Lol, that's still totally feasible for normal FIRE/retirement situations, my understanding is that most proposals only start at $50 million or more. You can still have a super cushy retirement with $3mil+ and 3% withdrawal forever.

> only start at $50 million or more

curious how they came to that number. There's probably plenty of voters willing to cast a vote for $0.5M+ and plenty ready to cast a vote for $100M+. How was the line drawn?

The minimum net worth of the top 1% of households is roughly $13.7 million[1]. So at $50 million they can say "we're only taxing the top of the top 1%" as a way to sell it.

"The top 1%" is a popular target for these schemes because 99% of people might be convinced to support it, since it won't affect them (at least not directly).

[1] https://www.investopedia.com/financial-edge/1212/average-net...

A wealth tax will affect the distribution of investments. It might make higher risk investments like stocks more attractive as compared to bonds, it might make them less attractive. More likely it might make publicly available instruments less attractive in general, as private investments have more flexibility in how they are evaluated. In any case, there will be winners and losers as the investment landscape shifts, which affects everyone. If equity becomes more attractive, it could force less wealthy people into equity, which means they will take on more risk. If private investments become more attractive, less wealthy people will lose out. It might not affect those with no assets, but that is not certain either. So, everyone will be affected, in some way. Impossible to model due to unintended side effects.

Yeah, "It won't affect the 99%," is the wrong framing. The entire point is for it to affect the 99% (by undoing the effect disproportionately high wealth among the wealthiest and disproportionately low wealth among the middle and least wealthy).

I think your assumptions are off, though; less wealthy people might not be "forced" into investment at all, but given the "opportunity" to pay off debt or increase/diversify consumption. In the end, the important part is the wealth transfer downward, wherever it ends up. No trickle, but you can pump it.

In 2020, there was a campaign (prop 15) to legalize increases on the property tax rate in California that only applied to commercial and industrial properties. Intuitively, the constituency for prop 15 should be very similar to a wealth tax on $0.5M+, since the set of people owning commercial/industrial real estate in California are mostly a subset of people with $0.5M+ wealth. What actually happened is there was heavy opposition and prop 15 was narrowly rejected by the voters. Organizations opposing the proposition included the American Legion, the NAACP, and California Beer and Beverage Distributors.

Arguably, there’s a disconnect where the people who lead civic organizations don’t have a great deal in common with the median member. They might be wealthier and generally more plugged in to power structures. They might not support policies that are in the best interest of members they represent, especially people who have a hard time representing themselves.

Anyway, if your goal is to get a policy enacted, it’s not enough for your policy to be theoretically good for the median voter. You need a winning political coalition.

There are probably good argument for it being lower (maybe circa $10 or $12 million. But I have a feeling they do want to try and not hit land-rich-but-otherwise-maybe-not "family farms" that have hundreds or thousands of acres.

Sort of like how the income tax in America started with it only applying to the top 1% of earners?

Do you remember when the top marginal tax rate was 90%? Things don't only move in one direction. The effective tax rate on the ultra wealthy has been steadily trending down for decades.

Today, sure. In 30 years I wouldn't expect to be able to retire with less that $50 million in savings.

I'm sure any wealth tax would only apply to wealth above a certain amount. For instance, inheritance tax only applies to $15mil and above. Likewise, when you sell a house the first $500K (I believe) in capital gains from the sale is tax free.

I don't think people with savings of $15mil and above (assuming that would be the cutoff) are in danger of going bankrupt in 20 yrs from a 1% wealth tax. Assuming your 3% return, they'd be earning $450,000 a year that wouldn't be touched by the wealth tax.

Sale of a house isn’t a wealth tax - that would be the property tax you pay, and the exclusions are pennies on the dollar on those.

No one is proposing a wealth tax on anyone other than the ultra-wealthy. If you are in a position where a 1% wealth tax would bankrupt you, then you probably aren't someone that it would apply to.

A sane taxation scheme should of course be paired with a humane social safety net that could pay you a comfortable pension.

But why wage earners should support you by paying more taxes? Reduce your spending by 33% to keep up.

I can't tell if this is sarcasm or a serious point.

Obviously people who have retired and based their entire life plan on making that work have many fewer options than those who are still working. You are arguing that nobody can plan for any kind of secure retirement, including you.

I also "had an Iron Man moment last week" as a mathematician. I've been doing joint math research with two friends (professors) on a project for several years. Last week, I decided to explore part of our research using chat GPT. 1) I would have a thought. 2) Present it to GPT. 3) Ask GPT to write theorems that were easy to prove and put those proofs into LaTeX. (I always have to check the proofs carefully.) 4) Then I would ask it to generate code (I mostly use Mathematica the language.) 5) Running the code would help verify the proofs. It would also inspire more thoughts and I would go back to step 2). This worked very well, but at one point I could not bound a particular expression and I was not understanding it well, so I got out the pencil and paper and redid the derivation myself which helped a lot. This whole process worked about 10 times faster than doing it without GPT. At the end of a couple of hours I had around 20 pages of correct proofs and all the code needed to do numerical simulations related to the proofs.

So why are you using ChatGPT?

> This whole process worked about 10 times faster than doing it without GPT.

ikrima, Do you have any links to your research or paper titles?

How about:

(* Mathematica Notation, Assume x>0 ) If[ x < 10^(-10), 1+ x/2, ( order x^2 error ) If[ x> 10^10, Sqrt[x], ( order 1/Sqrt[x] error ) (else) Sqrt[x +1] ] ] ( I guess the If statements take too much time. *)

HN formatter ate up the asterisks in your code comments :) To paste code blocks here, prepend each line with 2 or more spaces:

  (* Mathematica Notation, Assume x>0 *)
  If[ x < 10^(-10),  1 + x/2,   (* order x^2 error *)
  If[ x > 10^10,     Sqrt[x],   (* order 1/Sqrt[x] error *)
  (* else *)         Sqrt[x+1] ] ]
  
  (* I guess the If statements take too much time. *)