When you can formalize it in Lean or some such, why would this be? I can understand the desire to separate out other forms of research from the human corpus. But theoretical math that is decidable/provable, I’m not sure I see the risks.
I just want to state that having "lean proofs" that build does not mean the actual real theorems we care about hold. Ultimately a human has to verify the lean encoded theorem statements that the lean proofs are checked against. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal.
Agreed that confirming “This proposition has been faithfully translated to Lean” matters. As a side note, though, this is an area where LLMs used interactively can be helpful.
Also in the case of these recent counterexamples turning up, we have good qualitative evidence that this pathway is effective.
Because science is a branch of philosophy and machine existence brings plethora of unanswered questions.
Imagine humankind meets another race, another race shares it's scientific knowledge and humans accept it without experiencing process of discovery. In that case do we really got this knowledge? If we follow machine discoveries like we follow problems in textbook then we acquire knowledge but we don't discover anything. We follow.
There whole lot of philosophical questions that aren't attacked now. Are complex systems sentient because consciousness is emerging behavior? Then should they have rights? Philosophy is part of humanities and science (is/used to be) part of philosophy. Should we accept non-human knowledge in science? Maybe it's altogether different thing from science, yet very similar.
Perhaps this is a question of ethics. Should we come to a conclusion that human effort makes a text worth reading despite it's objective quality. Literacy is humanities by definition.
I started writing because AI made me obsolete in software development. Or at least gave me depression that blocks me from writing code. What I did instead I started writing my thoughts as short stories and then made an attempt to write full blown 50k words novel. It worked as therapy surprisingly well.
I write mostly without AI but then I use AI for editing and grammar correction. Sometimes when I struggle with plot threads I ask AI for an advice. When I write about something that a have a vague understanding about I may ask AI to write a paragraph or two. I'm also open about it and warn reader in preface and mark generated text using italics.
As a new author I find AI both helpful and discouraging, because it CAN write better prose than me. I think text that's written for humans should be written by humans, but temptation to ramp up quality with zero effort is huge.
Then I experimented with different regimes when I only allow myself a couple of prompts at the end of the day when I done writing and only allow minor edits. At least my conscience is clear.
Writing gives meaning, despite fact if anyone reads your stuff or not. Surely publishing a book is a major achievement but many authors wrote without publishing for many years. It's a therapy and getting a book printed is an achievement, but it's not mandatory.
It works like talking to yourself, your conscience and you also get a gut feeling about using AI in humanities with time. It starts to _feel_ bad if you go too far with it. It feels good when I write my text myself. Using AI for humanities feels like borrowing on bad terms.
If you're into simulators then you may try applying forces directly rather than integrating ODE. If sim's has tiny numerical instabilities or integrator schedule is wrong the whole thing gonna fall spectacularly. The interest is with running large-scale simulations where along with ODE you need to handle collisions and deformations. The best one currently is MuJoCo.
I learned a lot myself, but lately I just can't make it on stable regime because you don't get much positive feedback you you're learning something yourself. There's no grades, no exams and all of your motivation is internal. In that case you need to work on a motivation and goals. Why would you learn something that doesn't pays off then?
To improve your life, circumatances, abilities. To have a larger amount of known concepts to connect to each other. To increase your stability, security, quality of life, and self reliance. To make more money. To decrease your reliance on uncontrollable and unstable factors.
I'm quite fortunate to keep piling on knowledge without extrinsic rewards: the acquisition itself and the rewiring of my brain is what makes it enjoyable for me.
I look up to people who are well-read and try to follow their example. Maybe one day I can inspire somebody else.
I'm looking for an active (open-source) robotics projects with rust / python. I maintain robotics presence in rust-land with some of simulation-based crates (bevy_mujoco, bevy_urdf), and now looking for a projects that either solves real-world problems or a have steady interest.
well, maybe adopt an outlook that things you think are real aren't, and just maybe it will work just as fine if you completely ignore them. going forward ignoring ai that are smarter than autocomplete may be just the way to go
