I try to get it done within a day, so they don't back up, but I've never tried to compete. I am PST which opens at 9PM. I try to get through part 1 then, so I can sleep on part 2.
The subreddit /r/adventofcode contains discussions of solutions with lots of different skill levels.
I've done AoC for five years to learn new languages and try solve all of them myself during the month of December. (Dunno if I'll run the whole thing this year - I have another project.) Others try to get on the leaderboard, and some will implement solutions that they've seen sketched on reddit.
Last year a few people used Z3 for one of the problems, and I went back and tried that to get some experience with Z3. And I've occasionally gone back and tried another approach or new trick that I saw on the subreddit. (In the years that I've used Lean, I've sometimes gone back and added proofs for termination or array indices, too.)